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
pgp00000.pgp
Description: PGP signature
