|
Diese Diskussion wurde archiviert.
Es können keine neuen Kommentare abgegeben werden.
|
 |
|
|
|
Von Anonymer Feigling am Saturday 15. October 2005, 14:06 MEW (#1)
|
|
|
|
|
Die meisten "Hello world!" Programme sind absolut Fehlerfrei, bevor wieder einer kommt und behauptet es gibt kein fehlerfreies Programm...
|
|
|
|
|
|
|
|
|
|
|
Von Anonymer Feigling am Saturday 15. October 2005, 15:56 MEW (#2)
|
|
|
|
|
Hm, ganz so trivial ist das glaub ich nicht... zB in C müsste dann nämlich auch stdio.h fehlerfrei sein (schliesslich wirds benutzt um "Hello world!" auszugeben).
Abgesehen davon meine ich mich zu erinnern, dass einer meiner Uniprofessoren gesagt hat, dass es mathematisch bewiesen ist dass es nicht mathematisch beweisbar ist dass ein Programm fehlerfrei ist (was für ein komplizierter Satz)?!
|
|
|
|
|
|
|
|
|
|
|
|
|
Naja, das einzige was du mathematisch beweisen kannst, ist dass ein Programm einer Spezifikation entspricht. Ob die Spezifikation fehlerfrei ist... wer weiss? Für genau dieses Problem gibt's glaub ich einen Fachbegriff, der mir aber momentan nicht geläufig ist.
tL
--
... I don't like it, but I guess things happen that way ... (J. Cash)
|
|
|
|
|
|
|
|
|
Von Anonymer Feigling am Saturday 15. October 2005, 22:31 MEW (#4)
|
|
|
|
|
Lass mich raten: Kundenwunsch?
|
|
|
|
|
|
|
|
|
|
|
|
|
Das Problem des allgemeinen Korrektheitsbeweises lässt sich eigentlich immer auf das Halteproblem zurückführen.
D.h. der Prüf-Algorithmus soll 'lediglich' herausfinden ob der Eingabe-Algorithmus irgendwann terminiert.
Das Problem: Natürlich hängt das Terminieren eines Algorithmus von der zu lösenden Aufgabe ab -- und die kann zum Beispiel ein ungelöstes mathematisches Problem austesten.
Dann müßte der Prüf-Algorithmus automatisch den Sinn des zu prüfenden Algorithmus verstehen und das bislang ungelöste mathematische Problem lösen.
Oder -- die andere Möglichkeit er müßte den Prüf-Algorithmus ausprobieren -- aber dann terminiert der Test-Algorithmus genau dann wenn auch der Prüfling terminiert.
Man mag einwenden -- OK, aber für die Masse der Implementierungen trifft obiges nicht zu und der Prüfer kann zu einem Ergebnis kommen.
--> Rückfrage: Dann müßte es also einen Unterscheider zwischen Testbarer und Nicht-Testbarer Software geben....
--> Goto Anfang
Für weitere Überlegungen solcher Art empfehle ich das Buch "Gödel-Escher-Bach".
|
|
|
|
|
|
|
|
|
|
|
|
|
Mmmh.. Gödel, Escher, Bach... Das muss ich unbedingt noch fertig lesen.. Auch wenn ein, zwei Ansichten daraus unterdessen etwas "outdated" sind, finde ich das Buch sehr wertvoll.
tL
--
... I don't like it, but I guess things happen that way ... (J. Cash)
|
|
|
|
|
|
|
|
|
Von Anonymer Feigling am Tuesday 18. October 2005, 01:26 MEW (#10)
|
|
|
|
|
Es geht doch gar nicht darum, fuer jeden beliebigen Algorhytmus bzw. ein beliebiges Program zu beweisen, dass es korrekt sei bzw. zu einem Ende kommt. Es geht umgekehrt darum, Programme so zu schreiben, dass die Korrektheit beweisbar ist. Sicherlich gibt es auch unzaehlige Faelle und Probleme, wo dies niemals moeglich ist. Heutzutage werden allerdings nicht mal "triviale" Programme geprueft geschweige korrekt implementiert.
Ausserdem wird haeufig mit dem Halte-Problem argumentiert, wo keines existiert. Vorraussetzung scheint aber die Verwendung einer funktionalen Programmiersprache z.B. Haskell. Wenn jemand nun ein Bibliothek von Moduln erstellt, die auf Korrekt heit geprueft sind, dann ist es zumindest denkbar Software zu entwickeln, die in weiten Teilen auf korrektem Code basiert. Aehnliches ist ja Gang und Gaebe mit Java's JDK oder Eiffel's Entwicklungsumgebung, wobei die JDK sicherlich getestet aber wohl kaum mathematisch bewiesen korrekt ist.
Das bedeutet aber einen grossen Verzicht auf Individualitaet und Anpassung an Konventionen solcher Umgebungen. Das ist sicherlich schneller und sicherer aber ziemlich trocken. Solange Sprachen wie Eiffel oder Haskell nicht als "cool" angesehen werden und auch nur in Ansaetzen gelehrt werden, wird sich dies aber kaum durchsetzen, jedenfalls nicht im Open-Source Bereich.
|
|
|
|
|
|
|
|
|
|
|
|
|
Ich glaube das ist der feuchte Traum vieler Informatiker: Ein Program mathematisch beweisen zu können.
Mit ein paar Funktionen geht das ja, aber so allgemein habe ich meine Zweifel, ob das überhaupt das Ziel sein sollte.
|
|
|
|
|
|
|
|
|
Von Anonymer Feigling am Monday 17. October 2005, 22:24 MEW (#9)
|
|
|
|
|
Es ist bewiesen, daß niemand ein Programm schrei-
ben kann, das so eine Überprüfung macht.
Man kann beweisbar fehlerfreie Programme schreiben
(fehlt noch die Hardware). SPARC ist so ein An-
satz für eine Sprache.
|
|
|
|
|
|
|
|
|
|
|
|
|
Murphy's computers laws
Every non- trivial program has at least one bug
Corollary 1 - A sufficient condition for program triviality is that it have no bugs.
Corollary 2 - At least one bug will be observed after the author leaves the organization.
|
|
|
|
|
