Bei der Semantik von Programmiersprachen werden traditionell drei
Formen unterschieden: denotationelle Semantik, operationelle Semantik
und axiomatische Semantik. Die verschiedenen Formen von Semantik sind
für unterschiedliche Anwendungen geeignet: z.B. eine operationelle
Semantik als Grundlage für die Implementierung einer Sprache und
axiomatische oder denotationelle Semantiken zur Unterstützung von
Verifikationsaufgaben. Die Semantik-Formen stellen damit keine
Alternativen dar, sondern ergänzen sich hinsichtlich ihrer
Haupt-Anwendungsbereiche. Es ist daher sinnvoll, für eine
Programmiersprache miteinander konsistente Formen der Semantik zu
entwickeln. Im Rahmen des Verifix-Projekts wurde eine formale
generische Modellierung der Semantik-Formen für gängige
Programmiersprachkonstrukte zusammen mit den zugehörigen
mathematischen Grundlagen im Spezifikations- und Verifikationssystem
PVS entwickelt. Diese Modellierung ermöglicht es, in einem
einheitlichen formalen Rahmen die Beziehungen zwischen den
Semantik-Formen abzuleiten, so dass anschliessend etwa zum Beweis von
Eigenschaften einer operationellen Semantik eine denotationelle
Semantik, die von irrelevanten Details abstrahiert, herangezogen
werden kann. Wir stellen diese Modellierung vor als Grundlage für die
im Verifix-Projekt anfallenden Modellierungs- Verifikationsaufgaben.