On Fri, Feb 14, 2003 at 04:49:43PM +0000, Lutz Donnerhacke wrote: [...]
> > 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? Weil das keine komplizierten Eigenschaften sind. Halbwegs kompliziert w�re z.B. die Implementation eines Filesystems darauf zu testen, ob die Datenstrukturen auf der Platte immer konsistent bleiben. > > 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. Formal logische Aussagen sind isomorph zu Typen. Ein Verifikationstool kann deswegen auch nicht mehr, als was man in geeigneten Sprachen mit Typen machen kann. Das Problem ist, da� automatische Beweiser bei imperativen Sprachen nicht wirklich weit kommen. Seiteneffektfreie Sprachen sind ja gerade aus diesem Grund auf diesem Gebiet so beliebt. Gru�, Martin
pgp00000.pgp
Description: PGP signature
