* Martin Uecker wrote: > 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.
Mir nicht bekannt. > Beweis von Korrektheit setzt eine Spezifikation voraus. Korrekt. > Die kann aber auch fehlerhaft sein. Richtig. Man bemerkt dann aber schnell viele Specfehler. > Das ganze bringt also nicht so viel, wie man vielleicht denken k�nnte. Die Abwesenheit von Fehlerklassen bewiesen zu haben, bringt unheimlich viel. Z.B. keine Abst�rze mehr. Oder fester RAM Bedarf. Dann kann man das auf einen Chip/Platine gie�en ohne Angst haben zu m�ssen. Und f�r den Beweis der Abwesenheit von Laufzeitfehlern braucht man keine formale Spezifikation. > Aber selbst dann wird man f�r komplexe Programmsysteme, die in > imperativen Sprachen geschrieben sind, niemals irgenwelche komplizierten > Eigenschaften beweisen k�nnen. Beweis durch Behauptung? Warum klappt das dann in den o.g. Beispielen? > 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). Spark geht noch weiter und pr�ft die Imperativen Statements, den Informations- und Datenflu� und einige kleine Stilfragen. > 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. Richtig. Darum geht es hier nicht. Es geht darum, da� es machbar ist und gemacht werden sollte. Ob irgendwann mal mit Haskell oder jetzt und hier mit Spark.
