Programmverifikation in lauffähigen Pascal-Programmen

Wir haben eine Sprache PASQUALE-L entworfen, mit der einige neuere Konzepte aus der theoretischen Informatik wie Programmverifikation und abstrakte Datentypen fur lauffahige PASCAL-Programme verfugbar gemacht werden. Die Sprache ist in ein Verifikationssystem PASQUALE eingebettet, dessen Verification Condition Generator eine Implementierung der axiomatischen Definition von PASCAL ist. Die dort angegebene Verifikationsregel fur Prozedur-Aufrufe wird mit Hilfe einer Transformationsregel realisiert.