Entwurf eines sprachunabhängigen Verifikationssystems auf der Basis denotationaler Semantikbeschreibungen

Da Software in zunehmendem Maße auch in sicherheitsrelevanten Anwendungen eingesetzt wird, steigt der Bedarf an Software- Prüfung, die über das Testen hinausgeht. In dieser Arbeit wird ein System zur Prüfung von mit Zusicherungen angereicherten Programmen entwickelt, dessen Kern konstant ist und bei dem die sprachspezifischen Anteile aus der für die Erstellung eines Compilers vorhandenen Sprachbeschreibung generiert werden können. Die Grundidee für ein solches System besteht darin, Programme einer gegebenen Programmiersprache (z. B. Pascal) in eine Zielsprache zu übersetzen, das zielsprachliche Programm zu prüfen und anschließend die Prüfungsergebnisse rückzuübersetzen. Der Kernpunkt dieser Arbeit besteht zum einen darin, einen speziellen Begriff der Beweisprüfung einzuführen, der als Ergebnis nicht nur das Endergebnis der Prüfung liefert, sondern auch die Zwischenergebnisse. Hierfür wird eine Spezialisierung des üblichen Termbegriffes über einer heterogenen Algebra entwickelt, der die Annotation von Zwischenergebnissen an den Syntaxbaum zulässt. Zum anderen wird ein spezieller Kalkülbegriff entwickelt, der das Anhängen dieser Zwischenergebnisse an den Syntaxbaum realisiert. Schließlich wird dargestellt, unter welchen Umständen und wie diese Beweis(zwischen)ergebnisse in Bezug zu dem ursprünglichen Quellprogramm gesetzt werden können. Daneben wird dargestellt, wie die Integration eines solchen Beweissystems in eine Programmierumgebung vorzustellen ist. Um zu zeigen, dass die Mächtigkeit des Konzeptes auch für reale Anwendungen hinreichend ist, werden eine Beispiel-Zielsprache und ein Kalkül für diese Beispiel-Zielsprache vorgestellt. Bei dieser Sprache handelt es sich um eine Sprache erweiterter typisierbarer Lambda-Terme, die, wenn auch in anderer Form, für die Semantikdefinition von Programmiersprachen Verwendung findet.