Anhand von Fallbeispielen zeigen wir den Einsatz unseres Programmverifizierers NPPV für abstrakte Fragestellungen zwischen Mathematik und Informatik. Aus einem gegebenen und mit Invarianten annotierten Programmschema erzeugt das System automatisch logische Bedingungen für dessen Korrektheit.

Der Verifizierer wurde zum Einsatz im Informatikunterricht konzipiert. Er nimmt dem Benutzer die immer wiederkehrende Berechnung trivialer Verifikationsbedingungen ab und richtet die Aufmerksamkeit und die Kreativität auf das Wesentliche - aussagekräftige Invarianten, Axiome der verwendeten Datenstrukturen, Existenz von Funktionen mit bestimmten Eigenschaften.

Der Schwerpunkt liegt auf der Verifikation abstrakter Programme (Pro-grammschemata), z.B. zur Transformation zwischen rekursiven und ite-rativen Programmen. Selbst die Äquivalenz zwischen einem abstrakten Induktionsbeweis und der Verifikation eines Programmes, welches ein Gegenbeispiel zur Behauptung sucht, läßt sich mit NPPV interaktiv er-kunden.