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.:
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.