New Paltz Program Verifier

New Paltz Program Verifier (kurz NPPV) ist ein Programmverifizierer für einfache WHILE-Programme. Er entstand, als der Autor noch Professor an der State University of New York, College at New Paltz, war. Gegenwärtig wird NPPV im Rahmen einer Diplomarbeit weiterentwickelt. Demnächst wird es auch eine Windows95 und WindowsNT-Version geben.

Für eine Einführung in die Grundbegriffe der Programmverifikation verweisen wir auf Kapitel 2.9 "Verifikation" in unserem Lehrbuch "Einführung in die Informatik".

NPPV ist ein komplettes Programmiersystem so wie viele Programmierer es von gängigen Programmiersprachen (z.B. Turbo-Pascal) gewohnt sind. In einem Editor wird ein annotiertes Programm erstellt und aus einem Menue kann man verschiedene Funktionen aufrufen. Die wichtigste ist : Prove. Diese Funktion erzeugt aus dem annotierten Programm sogenannte Verifikationsbedingungen. Sie werden nach Möglichkeit auch sofort bewiesen. Gelingt dies nicht, so werden sie vereinfacht und als "Remains to Prove" angezeigt. Sind alle Verifikationsbedingungen gültig, so erfüllt das Programm seine Spezifikation.

Besonders interessant an NPPV ist, daß auch "abstrakte Funktionen" und "abstrakte Prädikate" verwendet werden können. Auf diese Weise kann NPPV aus einem annotierten Programm Bedingungen an die Datentypen oder an die Invarianten generieren, die eine Korrektheit garantieren. Zahlreiche Beispiele für die Verifikation abstrakter Programme haben wir in dem Artikel "Generating Algebraic Laws from Imperative Programs"  demonstriert.

Neben den Beispielen zur Verifikation einfacher Standardprogramme gehören zu dem NPPV-System Dateien für die Verifikation allgemeinerer Programme oder Programmschemata, z.B.:

Das NPPV-System ist frei verfügbar (mit WinZip komprimiert, oder als selbstextrahierendes Archiv). Über eine Rückmeldung oder auch über weitere Anwendungsbeispiele würde ich mich freuen.

Neuerdings gibt es auch eine Java-Variante - jpv. Es verwendet die Syntax einer kleinen Teilmenge von Java und es ist in Java geschrieben und als jar-File vorhanden.