Automatische Verifikation?

Automatisches Beweisen von Programm-Eigenschaften ist praktisch unmöglich.

(Satz von Gödel, Turing:  Halteproblem ist nicht entscheidbar.)

D. h., der Programmierer muß mithelfen: Programm und Beweis gleichzeitig schreiben.

Werkzeuge können verifizieren, daß beides zueinander paßt.

Simples Beispiel: Programm und Typ-Deklarationen.



Johannes Waldmann 2006-06-26