* Martin Uecker 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.
Ich halte fest: Hubschraubersteuerungen und CA-Systeme nicht trivial im Vergleich zu Filesystemen. Man lernt auf debate immer dazu. >> 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. Ich kann Dir gerade nicht folgen. Wie beweist man durch Angabe eines (skalaren) Typs, da� in dem Ausdruck "4*len/3" kein �berlauf auftritt? Bitte per eMail, f�r debate ist das zu speziell. > 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. Seiteneffektfreiheit kann mit mit Datenflu�analyse zeigen. Es ist nicht notwendig, da� alle Sprachkonstrukte diese Eigenschaft haben. Und man spart sich die Monade der Welt.
