Bugs in der STL

[knivil]

fghjrtzedrtsdf schrieb:

knivil schrieb:

Innerhalb des Prozesses koennen Fehler gemacht aber korrigiert werden. Wo ist das Problem?

Dass es scheinbar keinem außer Dir gelingt. Es gibt keinen Prozess der so idiotensicher ist, dass jeder Fehler vermieden werden kann.

Warum sollten Prozesse Idiotensicher sein? Wozu benoetigt man dann noch Entwickler? Warum ist fehlerfreie Software so abwegig? Wieso schert sich jeder einen Dreck drum?

Ich dachte bisher Du hättest Erfahrung und Ahnung. Das hätte sich mit diesem Thread erledigt.

Ich gebe nichts auf meine Popularitaet, dass du mich achtest oder respektierst.

[MetaPeter]

knivil schrieb:

fghjrtzedrtsdf schrieb:

knivil schrieb:

Innerhalb des Prozesses koennen Fehler gemacht aber korrigiert werden. Wo ist das Problem?

Dass es scheinbar keinem außer Dir gelingt. Es gibt keinen Prozess der so idiotensicher ist, dass jeder Fehler vermieden werden kann.

Warum sollten Prozesse Idiotensicher sein? Wozu benoetigt man dann noch Entwickler? Warum ist fehlerfreie Software so abwegig? Wieso schert sich jeder einen Dreck drum?

Da Menschen Fehler machen und auch machen müssen, ansonsten würde sie sich nie weiter entwickeln, sind auch alle Werke der Menschen mit Fehlern behaftet. Lernen beispielsweise funktioniert nur durch Fehler machen.

Die ganze Evolution beruht auf Fehlern.

Zusätzlich kann das Gehirn des Menschen schlecht objektiv oder im Ganzen denken.

Da wird jetzt aber eine Metadiskussion hier. Also entweder zeigt Knivil nun Einsicht und begreift, warum es keine fehlerfreie Software von Menschenhand geben kann, oder er lässt es halt. Vielleicht findet er wirklich einen Weg 100% fehlerfreie Software zu schreiben und erlangt dann recht schnell Weltrum.

Vielleicht findet es noch heraus wie Gravitation funktioniert und eliminiert oder eliminiert die ganzen Naturkonstanten, damit auch mal die Physik frei von Fehlern wird. Es gibt meines Wissen nämliche keine Naturwissenschaft ohne massig Fehler durch mangelndem Wissen. Es gibt viel mehr Annäherungen und Tricks in den Wissenschaften als wirkliches 100% Wissen. Und das Bild von der Welt, dem Universum oder auch dem Menschen wird sich wohl noch so einige Male komplett wandeln.

Das was wir heute wissen ist ein Witz.

[osdt]

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

[inkompetent]

fghjrtzedrtsdf schrieb:

knivil schrieb:

Innerhalb des Prozesses koennen Fehler gemacht aber korrigiert werden. Wo ist das Problem?

Dass es scheinbar keinem außer Dir gelingt. Es gibt keinen Prozess der so idiotensicher ist, dass jeder Fehler vermieden werden kann.

Ich dachte bisher Du hättest Erfahrung und Ahnung. Das hätte sich mit diesem Thread erledigt.

Au ja, ich hatte ihm sonst auch eine Kernkompetenz zugeschrieben. Wenn jetzt eine Antwort von ihm kommt, warte ich lieber noch eine andere ab.

[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.

[Fehlerkette]

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.

[kleiner Troll]

@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.

[nwp3]

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.

[decimad]

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...