Bugs in der STL

Skym0sh0

osdt schrieb:

Q: ist es möglich komplexe Software 100% fehlerfrei zu entwickeln?
A: theoretisch ja!

Eine Theorie bleibt eine Theorie bis sie bewiesen werden kann

- osdt

Ich schmeisse einfach mal so theoretische Dinge wie das Hoare-Kalkül und den Satz von Rice in den Raum.

Und daran angeknüpft: Wer meint sein Programm sei fehlerfrei - Beweis oder zählt nicht (auch den Quellcode zeigen reicht nicht! Nur der theoretische Beweis).

hustbaer

Skym0sh0 schrieb:

Und daran angeknüpft: Wer meint sein Programm sei fehlerfrei - Beweis oder zählt nicht (auch den Quellcode zeigen reicht nicht! Nur der theoretische Beweis).

Der theoretische Beweis ist, genau so wie ein Programm, ein formales Konstrukt, das fehlerhaft sein kann.
Wenn du sagst "Quellcode zeigen reicht nicht", musst du konsequenterweise auch sagen "Beweis zeigen reicht nicht" - denn dann müsste man erstmal die Korrektheit des Beweises beweisen.
Wo sich dann der Hund in den Schwanz beisst.

Selbst wenn es möglich wäre 100% fehlerfreien Sourcecode zu schreiben, dann bleiben immer noch fehlerhafte Compiler, Linker, OS, Treiber, Hardware in der Kette stehen. Mal von Designfehlern in der Planung abgesehen.

@hustbaer
Prinzipiell hast du zwar nicht völlig unrecht, allerdings kann man unter der Annahme das die elementare Logik korrekt ist (und praktisch nimmt man das immer an)durchaus Beweise die gültig sind machen. Aber eben nicht für jedes Programm, die allgemeine Unlösbarkeit des Halteproblems verbietet das. (Zur kleinen Erklärung: Für jedes beliebiges Programm kann man es dann als "korrekt" ansehen wenn es hält. Könnte man also die Korrektheit allgemein zeigen, könnte man auch das Halteproblem lösen. Da das aber nicht geht, kann man im allgemeinen nicht die Korrektheit zeigen)

Damit will ich sagen, das "Richtigkeit eines Programms" eine deutlich andere - viel stärkere - Aussage als "Richtigkeit des Beweises" ist.

Und wenn postuliert das die mathematische Logik korrekt ist, muss man auch Beweise nicht mehr beweisen, deine Rekursionsversuch schlägt also fehl.

Fehlerkette schrieb:

Selbst wenn es möglich wäre 100% fehlerfreien Sourcecode zu schreiben, dann bleiben immer noch fehlerhafte Compiler, Linker, OS, Treiber, Hardware in der Kette stehen. Mal von Designfehlern in der Planung abgesehen.

Es geht um korrekte Software. Ziel ist es nicht die Korrektheit des Universums zu beweisen. Alles was du nennst ist nicht Teil der Software.

knivil schrieb:

Was fehlt dir, um siche Software zu entwickeln?

Annahme: sicher = korrekt.
Eine Grammatik fehlt. Eine Grammatik, die nur korrekte Programme erzeugen kann. Wenn man die hätte, dann könnte man jedes Programm mehr oder weniger trivial auf Korrektheit prüfen. Die Grammatiken heute finden lexikalische, syntaktische und meinetwegen auch semantische Fehler. Aber sie übersehen logische Fehler.

int getKmInM(int km){
    return km / 1000; //upsi
}

Die Funktion ist Teil eines aus Sicht heutiger Grammatiken völlig korrekten Programms. Aber sie ist falsch. Aufgabe: Finde ein System, was diese Funktion als falsch erkennen würde. Oder ein System, dass die Konstruktion einer solchen Funktion nicht zulässt. Ich kann mir keins vorstellen.

knivil

Eine Grammatik fehlt. Eine Grammatik, die nur korrekte Programme erzeugen kann.

Die gibt es fuer ausgewaehlte Domains sicher.

im allgemeinen ... jedes Programm

Es geht aber nicht um jedes Programm.

Traurig, dass man darüber ewig diskutieren muss

Traurig, dass alle einfach nur baschen wollen.

hustbaer

@kleiner Troll
Was du schreibst geht leider total an der Realität vorbei.
Du kannst Korrektheitsbeweise leider nicht automatisieren, bzw. keine breit anwendbaren Beweise entwickeln.

Und zwar deswegen nicht, weil "korrekt wenn hält" oder ähnliche einfache, "universelle" Definitionen von Korrektheit totaler Schwachsinn sind.
Üblicherweise schreibt man Programme, um aus einem gegebenem Input einen bestimmten Output zu erzeugen. Und üblicherweise sind die Regeln nach denen das zu passieren hat recht komplex.

Um zu beweisen dass das Programm korrekt ist, musst du beweisen dass es der Vorgabe entspricht. Dass es die definierten Regeln umsetzt.

Dazu brauchst du aber erstmal eine Beschreibung der Regeln. Und zwar eine, die du automatisiert weiterverarbeiten kannst. Oder auf die du zumindest Transformationen anwenden kannst, deren Korrektheit automatisiert überprüfbar ist.
D.h. du musst die Regeln in einer formalen Sprache ausdrücken.

In einer formalen Sprache, wie z.B. ... Lisp.
Und fällt dir was auf? Richtig, jetzt hast du ein Lisp Programm. Und dein toller, semi-universeller Beweis hat bewiesen dass dein XYZ Programm dem Lisp Programm entspricht. Uh yeah bebe, ur a winna!

Und fällt dir noch was auf? Man hätte sich gleich sparen können das XYZ Programm zu schreiben. Schliesslich gibt es Lisp interpreter.

Und fällt dir noch noch was auf? Richtig. Du musst jetzt beweisen dass das Lisp Programm "korrekt" ist - in dem Sinn dass es den Vorgaben entspricht.

knivil

korrekt wenn hält

Die Frage nach der Terminierung eines Programms kann fuer viele Programme (unendlich viele) entschieden werden, fuer viele nicht. Das gleiche gilt fuer Fehlerfreiheit bzw. eine Eigenschaft X.

Btw. haben hier recht wenige begriffen, dass es nicht um mein Programm im Speziellen geht. Es geht um die Existenz fehlerfreier Software im allgemeinen. Diese Fehlerfreiheit muss auch nicht zwingend formal bewiesen werden, da beispielsweise der Konstruktionsprozess das eben garantiert.

Desweiteren verstehe ich nicht, warum fehlerfrei Software dermassen auf Widerstand stoesst. Uebertragen beisielsweise auf fehlerfreie Bruecken: Eigentlich duerfte die Golden-Gate-Bridge oder jene ueber unseren kleinen Bach nicht benutzt werden, da damit gerechnet werden muss, dass sie einstuertzt. Als Argumentation wird dann immer die Tacoma Narrows Bridges angefuehrt.

Du musst jetzt beweisen dass das Lisp Programm "korrekt" ist

In Pearls of Functional Algorithm Design wird ebenfalls von einem Programm ausgegangen, dessen Korrektheit leicht bewiesen werden kann aber ineffizient ist. Durch aequivalente Umformungen wird es in ein effizientes Programm transformiert. Du siehst, es ist nicht zwingend problematisch ein weiteres Programm als Ausgangspunkt zu haben.

Shade Of Mine

knivil schrieb:

Desweiteren verstehe ich nicht, warum fehlerfrei Software dermassen auf Widerstand stoesst.

Weil noch nie eine Fehlerfreie Software in der freien Wildbahn gesichtet wurde. Nicht eine einzige.

PS:
Auch Brücken sind nicht Fehlerfrei. Müssen sie auch nicht sein. Es reicht wenn sie ihre Aufgabe erfüllen.
Gleiches gilt für Software. Der aktuelle Linux Kernel ist zB auch nicht Fehlerfrei, erledigt seinen Job aber ziemlich gut.

knivil

freien Wildbahn

Haeh? Es gibt mindestens eine Firma, die in ausgewaehlten Bereichen die Fehlerfreiheit wahrscheinlich garantieren kann: http://corp.galois.com/ . Ich arbeite nicht dort, deswegen ist das keine sichere Aussage.

Bashar

hustbaer schrieb:

Und zwar deswegen nicht, weil "korrekt wenn hält" oder ähnliche einfache, "universelle" Definitionen von Korrektheit totaler Schwachsinn sind.

Wer denkt sich sowas aus? Die Definition von Korrektheit ist, dass das Verhalten einer vorgegebenen Funktion entspricht. Da gibts nichts dran zu rütteln. (Natürlich ist das über den Satz von Rice äquivalent zum Halteproblem [eines anderen Programms], vielleicht meinst du das.)

D.h. du musst die Regeln in einer formalen Sprache ausdrücken.

In einer formalen Sprache, wie z.B. ... Lisp.

Warum nicht C++, das ist auch eine formale Sprache. Oder Brainfuck.

Und fällt dir was auf? Richtig, jetzt hast du ein Lisp Programm. Und dein toller, semi-universeller Beweis hat bewiesen dass dein XYZ Programm dem Lisp Programm entspricht.

Mir scheint, du fällst grade über deinen eigenen Strohmann.

Und fällt dir noch was auf? Man hätte sich gleich sparen können das XYZ Programm zu schreiben. Schliesslich gibt es Lisp interpreter.

Ich glaube nicht, dass Korrektheit bewiesen wird, indem man dasselbe Programm nochmal in einer anderen Programmiersprache schreibt. Um beispielsweise einen Sortieralgorithmus zu spezifizieren, genügt es, in irgendeiner Form auszudrücken, dass zu einer Liste $(a\_1,\ldots,a\_n)$ eine Permutation $\sigma\in S_n$ gefunden wird, so dass $(a_{\sigma(1)} \leq a_{\sigma(2)} \leq \cdots \leq a_{\sigma(n)})$ . Ich hab sowas noch nie gemacht, wahrscheinlich ist es schwerer als ich es mir vorstelle, aber mit Sicherheit nicht so wie du dir es dir vorstellst.

hustbaer

@nwp3
Dein getKmInM zeigt finde ich ganz gut das eigentliche Problem.
Das kann man in C++ nämlich sehr einfach "sicher" hinbekommen. Indem man Längen nicht als Integers behandelt, sondern einen eigenen Typ dafür macht.

Jetzt kannst du natürlich argumentieren "ja, aber C++ lässt es mich eben auch falsch schreiben". Und genau das ist das Problem: jede Sprache wird dich "falsche" Dinge hinschreiben lassen, die formal korrekt sind. Weil die Frage ob etwas "falsch" ist davon abhängt was man haben wollte. Und die Programmiersprache kann das ja schlecht wissen. Wüsste sie es, dann müsste man ja nichts mehr programmieren.

hustbaer

Achjeh...

Bashar schrieb:

Die Definition von Korrektheit ist, dass das Verhalten einer vorgegebenen Funktion entspricht.

Ja, genau da liegt der Hund begraben.
Die "vorgegebenen Funktion" muss erstmal exakt formuliert werden.
Und wie nennt man das? Das nennt man Programm. (OK, man kann es auch anders nennen, Algorithmus, Formel - whatever. Macht aber keinen echten Unterschied - ist im Endeffekt alles das selbe.)

Deine Argumentation läuft auf "works as implemented == korrekt" hinaus.
Mit dieser Definition von korrekt kann ich aber nichts anfangen, die ist für nix gut.

Bashar

hustbaer schrieb:

Achjeh...

Bashar schrieb:

Die Definition von Korrektheit ist, dass das Verhalten einer vorgegebenen Funktion entspricht.

Ja, genau da liegt der Hund begraben.
Die "vorgegebenen Funktion" muss erstmal exakt formuliert werden.
Und wie nennt man das? Das nennt man Programm. (OK, man kann es auch anders nennen, Algorithmus, Formel - whatever. Macht aber keinen echten Unterschied - ist im Endeffekt alles das selbe.)

Doch, das macht einen grundlegenden Unterschied, weil ein Algorithmus effektiv und normalerweise auch effizient sein muss. Siehe mein Sortierbeispiel. Es gibt viele Probleme, deren Lösung einfach zu definieren aber schwer zu finden ist.

Mann Jungs, das einzig interessante hier im Thread war doch, ob knivil auch nur mit Wasser kocht (nachdenken und testen). Ob er das Resultat als fehlerfrei betrachtet oder auch nicht ist doch völlig Rille für unser aller weiteres Vorgehen.

Um hier wirklich eine fruchtbare Diskussion auf theoretisch abstraktem Niveau zu führen, denkt doch ein jeder (ich nehme mich da nicht aus) zu wenig über seine Kommentare nach und dann verliert sich alles in punktuellen Korrekturen etc...

Ist es nicht genug?

Shade Of Mine

knivil schrieb:

freien Wildbahn

Haeh? Es gibt mindestens eine Firma, die in ausgewaehlten Bereichen die Fehlerfreiheit wahrscheinlich garantieren kann: http://corp.galois.com/ . Ich arbeite nicht dort, deswegen ist das keine sichere Aussage.

Können sie oder können sie nicht?
Ein wahrscheinlich ist ein bisschen schwach Die Webseite lädt bei mir aber nicht, was nicht unbedingt für Fehlerfreiheit spricht

PS:
Du behauptest fehlerfreie Software wäre kein Problem, aber ein Beispiel für Fehlerfreie Software liefern kannst du nicht. Mhm...

knivil

Du behauptest fehlerfreie Software wäre kein Problem

Nein, das behaupte ich nicht. Ich widerspreche der Aussage, das fehlerfreie Software nicht unmoeglich ist, und in speziellen Faellen wenig Aufwand bedeutet. Diese speziellen Faelle sind nicht trivial und sehr verschieden von "Hello World".

aber ein Beispiel für Fehlerfreie Software liefern kannst du nicht.

Bspw. Space Shuttle Software. So, aber das ist nicht die Software von der ich eigentlich nicht rede oder reden moechte, da die verfuegbaren Ressourcen fuer das Projekt nicht mit einem Kalibriertool bspw. korrelieren.

knivil auch nur mit Wasser kocht

Nee, es geht mir nicht um mich. Euch anscheinend schon. Das Beispiel kommt aus meiner "Erfahrung" und ihr wollt mir nachweisen, dass ich halluziniere. Es geht auch nicht um immer und allgemein auch nicht.

Was soll der Scheiss, warum wird mein Standpunkt absichtlich verzerrt? Nur damit eurer Gebasche besser passt ... Hand hoch, wer Software fuer Medizinprodukte herstellt!

Die Webseite lädt bei mir aber nicht, was nicht unbedingt für Fehlerfreiheit spricht

Ich haette gern einen formalen Beweis, dass die Seite bei dir nicht laedt. Ich glaube du halluzinierst.

Shade Of Mine

knivil schrieb:

Bspw. Space Shuttle Software. So, aber das ist nicht die Software von der ich eigentlich nicht rede oder reden moechte, da die verfuegbaren Ressourcen fuer das Projekt nicht mit einem Kalibriertool bspw. korrelieren.

Es gibt viele prominente Beispiele von Fehlern in Raketen-Software.

Hand hoch, wer Software fuer Medizinprodukte herstellt!

Ich hab auch ein paar Beispiele aus der Medizin wo Softwarefehler zu richtig bösen Fehlern geführt haben.

ich warte weiter auf ein Beispiel. Ein einziges Beispiel.
Kann ja nicht so schwer sein, oder?

Und ich dachte, Dein Standpunkt wäre, dass fehlerfreie Software nicht unmöglich wäre! Jetzt widersprichst Du diesem Standpunkt?

hustbaer schrieb:

@nwp3
Dein getKmInM zeigt finde ich ganz gut das eigentliche Problem.
Das kann man in C++ nämlich sehr einfach "sicher" hinbekommen. Indem man Längen nicht als Integers behandelt, sondern einen eigenen Typ dafür macht.

Wenn man einen eigenen Typ macht, dann ist dort auch die getKmInM-Funktion drin, genauso falsch wie vorher. Es ist natürlich sinnvoll dafür einen Typen zu machen, weil man nur noch an einer Stelle diesen Fehler machen kann, aber man kann ihn trotzdem machen.

Dagegen hilft möglichst viele Leute mit Ahnung drüber kucken lassen und hoffen, dass es wem auffällt.

Unit-Tests könnten den Fehler auch finden. Oder 2 Implementierungen, wo dann ein System versucht einen Widerspruch zu finden und man dann nachprüfen kann wer recht hatte. Und hoffen, dass niemals in beiden Implementierungen der gleiche Fehler vorkommt.

Alles zu viel hoffen.

decimad schrieb:

Mann Jungs, das einzig interessante hier im Thread war doch, ob knivil auch nur mit Wasser kocht

Ist mir egal womit knivil kocht. Interessant ist, ob man die Korrektheit von Software beweisen kann.

Folgender Ansatz funktioniert ganz gut: Unterteilung in Fehlerklassen. Fehlerklassen Lexik/Syntax kriegt der Compiler hin, Semantik mit Einschränkungen. Bufferoverflows, Memory Leaks, Race Conditions und Integer Overflows kann man per Unit Test testen, indem man alle gültigen Eingaben durchprobiert und es nachprüft, dauert nur etwas.
Sanity Checks können grobe Fehler wie eine falsche Umrechnung finden, aber versagen bei falschen plausibel aussehenden Resultaten.
Rundungsfehler kriegt man sicher auch weg, indem man immer in eine Richtung rundet und dann einen Bereich angibt, in dem das Ergebnis liegt.

Am Ende gibt man dann eine Liste von Fehlerklassen an und kann jeweils sagen, ob es einen Fehler in dieser Fehlerklasse geben kann. Man kriegt nicht alle Fehlerklassen weg und man kann auch nicht garantieren alle Fehlerklassen betrachtet zu haben, aber es ist ein Anfang.

Es gibt noch einen Punkt der eigentlich aus der Security Ecke kommt. Man hat formal bewiesen, dass der neue elektronische Personalausweis unknackbar ist. 3 Wochen später wurde er geknackt. Was ist passiert? Im Beweis stand eine Annahme, die man kaputt gemacht hat. Irgendwo wurde irgendwas am Ausweis verändert, was im Beweis nicht vorgesehen, aber praktisch möglich war. So ein Beweis macht es übrigens allgemein recht einfach Lücken zu finden, weil man die Voraussetzungen durchgeht und eine davon kaputt machen kann.