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