On Thu, Feb 13, 2003 at 04:55:57PM +0000, Lutz Donnerhacke wrote: > > Eigentlich nie, oder kennst Du ein Beispiel? > > Das CA System von Mondex, Hubschrauber, Rakten und Flugtechnik. Mißverständnis. Ich wollte eigentlich wissen, ob es ein Open Source-Projekt gibt, das sowas macht. > > Und selbst dann heißt "Abwesenheit aller Laufzeitfehler" auch nur, daß > > die Runtime-Umgebung nicht kollabiert, und keineswegs, daß das Programm > > zur Laufzeit keine Scheiße baut. > > Es sind drei Schritte: > - Abwesenheit von Laufzeitfehler heißt: Keine Bereichsüberschreitungen > für Feldgrenzen, Überläufe in der Arithmetik, keine Division durch Null, > etc. pp. Das kann man maschinell beweisen. > - Partielle Korrektheit. Das kann man maschinell beweisen. > - Totale Korrektheit. Das ist nach der partiellen Korrektheit leichter, > wird nicht maschinell angeboten. > > Maschineller Beweis heißt, daß man ca. 90% des Codes als Korrekt abharken > kann und der Rest mit konktreten Randbedingungen hochschlägt. Beweis von Korrektheit setzt eine Spezifikation voraus. Die kann aber auch fehlerhaft sein. Das ganze bringt also nicht so viel, wie man vielleicht denken könnte. Aber selbst dann wird man für komplexe Programmsysteme, die in imperativen Sprachen geschrieben sind, niemals irgenwelche komplizierten Eigenschaften beweisen können. Aber es gibt Sprachen, die beweistechnisch wesentlich einfacher zu behandeln sind, und selber schon eine Art Spezifikationssprache in Form eines mächtigen Typsystems eingebaut haben. Meckert der Typechecker nicht, hat das Programm die im Typ spezifizierten Eigenschaften (siehe Curry-Howard-Isomorphismus). Das ist in heute verfügbaren Sprachen wie Haskell noch kaum ausgereizt, aber z.B. Haskell ist IMHO schon heute der bessere Weg zu robuster Software als Ada + Z. Vielleicht nicht für Raketensteuerungen - aber darum ging es hier nicht. Gruß, Martin
Attachment:
pgp00003.pgp
Description: PGP signature