Operationelle Semantik
Die operationelle Semantik ist eine Technik der Informatik um die Bedeutung beziehungsweise die Semantik von Computerprogrammen zu beschreiben. Die Wirkung eines Programms wird aufgefasst als schrittweise Zustandsänderung einer abstrakten Maschine. Operationelle Semantik wird verwendet, um Eigenschaften einzelner Programme nachzuweisen oder Programme zueinander in Beziehung zu setzen.
Zentral für die operationelle Semantik ist der Begriff des Programmzustands. Ein Zustand beschreibt dabei (in den meisten Fällen) eine Belegung der Programmvariablen sowie eine Position im Programm. Des Weiteren wird definiert, wann und wie sich Zustände ändern. Dies geschieht entweder mit Hilfe einer Zustandsübergangsfunktion oder durch sogenannte Inferenzregeln (also regelbasiert). Zustandsübergangsfunktion bzw. Inferenzregeln definieren einen Interpreter.
Um mit der operationellen Semantik eines Programms zu arbeiten, wird in der Regel ein kleines Stück vom Originalprogramm abstrahiert. Es wird ein abstraktes Programm aufgestellt, das äquivalent zum Original (dem konkreten Programm) ist und das durch einen abstrakten Interpreter ausgeführt werden kann. Die Wirkungen, die dieses abstrakte Programm auf die Zustände der abstrakten Maschine erzeugt, sind dann äquivalent zu den Zuständen, die erhalten werden, wenn das konkrete Programm ausgeführt wird.
Ein Spezialfall der Operationellen Semantik ist die Strukturierte Operationelle Semantik (SOS), die von Gordon Plotkin eingeführt wurde.
Beispiele für die Verwendung von operationeller Semantik sind die Semantikspezifikationen von Algol 60, PL/I oder VDL.
Neben der operationellen Semantik gibt es auch die denotationelle Semantik und die axiomatische Semantik, um die Semantik von Computerprogrammen zu beschreiben.
Literatur
- Hanne Riis Nielson, Flemming Nielson: Semantics With Applications - A Formal Introduction.John Wiley & Sons. 1992