ComLisp, eine applikative Teilsprache von Common Lisp mit imperativen
Bestandteilen, Zuweisung, sequentieller Komposition und Schleifen, ist
sorgfältig gewählte Quell- und Übersetzer- oder
Systemimplemetierungssprache in Verifix. Der applikative Teil findet
sich auch in der Logik des neuen Boyer-Moore-Theorembeweisers ACL2
wieder. Der Vortrag zeigt, wie ACL2 mechanische Korrektheitsbeweise
für applikative ComLisp-Programme erlaubt. Totaler Korrektheitsbeweis
in ACL2-Logik geht ohne weitere Beweisverpflichtungen in partiellen
Korrektheitsbeweis für das ComLisp-Programm über, Erhalten partieller
Korrektheit als Implementierungsbegriff überträgt schließlich
partielle Korrektheit auf das binäre ausführbare Maschinenprogramm,
von dem somit nachgewiesen ist, daß im Falle regulären Terminierens
das Resultat korrekt im Sinne des Quellprogrammes ist, daß der
Benutzer sich auf die Resultate von Programmläufen verlassen kann. Als
Fallstudie wählen wir einen kleinen Theorembeweiser, eine
Entscheidungsprozedur für aussagenlogische Tautologien.