Um bestehende Programme zu verstehen, die Korrektheit sicherheitskritischer Systeme zu gewährleisten oder eine eindeutige Interpretation von Modellen zu erreichen, ist es bei der Entwicklung von Software erforderlich sich mit der Bedeutung (Semantik) von Programmen und Anforderungen auseinanderzusetzen. Eine formale Semantik der verwendeten Programmier- und Spezifikationssprachen hilft dabei Fehler zu vermeiden, eröffnet den Zugang zu Rechnerunterstützung für Beweise und schafft Klarheit im Zweifelsfall.

Die Unifying Theories of Programming von Hoare und He beschreiben die Semantik von Spezifikationen und Programmen unterschiedlicher Sprachparadigmen in einem gemeinsamen Formalismus. Im Mittelpunkt steht die Modellierung nichtdeterministischer, imperativer Programme durch spezielle mathematische Konstrukte, sogenannte Relationen, die den Ablauf eines Programms durch die Änderungen seines Zustands beschreiben. Sie bilden eine solide Grundlage für den Aufbau weiterer Theorien, schränken aber den Anwendungsbereich unnötig ein.

Herr Dr. Walter Guttmann leistet mit seiner Dissertation zwei wesentliche Beiträge zum Gebiet der formalen Semantik von Programmiersprachen. Seine allgemeinere, algebraisch basierte Darstellung der Unifying Theories of Programming klärt die zugrundeliegende Struktur, vereinfacht Rechnungen und Beweise (siehe Beispiel unten), macht bestehende Mathematik anwendbar und integriert weitere Ansätze zur Semantik. Die von ihm definierte neue Theorie ermöglicht adäquate Fehlerbehandlung, die Modellierung sogenannter nicht strikter Berechnungen sowie Effizienzsteigerungen durch die Übertragung der verzögerten Auswertung von funktionalen auf imperative Programmiersprachen. Beide Fortschritte wirken mit, um Programme auf einer höheren Abstraktionsebene zu entwickeln und so der zunehmenden Komplexität von Software zu begegnen.