Operationale Semantik
aus Wikipedia, der freien Enzyklopädie
Die operationale 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. Operationale Semantik wird verwendet, um Eigenschaften über einzelne Programme nachzuweisen oder Programme zueinander in Beziehung zu setzen.
Zentral für die operationale 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 operationalen Semantik eines Programms zu arbeiten, wird in der Regel ein Stück weit 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 Operationalen Semantik ist die Strukturell Operationale Semantik (SOS), die von Gordon Plotkin eingeführt wurde.
Beispiele für die Verwendung von operationaler Semantik sind die Semantikspezifikationen von Algol 60, PL/I oder VDL.
Neben der operationalen Semantik gibt es auch die denotationale Semantik und die axiomatische Semantik, um die Semantik von Computerprogrammen zu beschreiben.
Siehe auch: Formale Semantik
[Bearbeiten] Literatur
- Hanne Riis Nielson, Flemming Nielson: Semantics With Applications - A Formal Introduction.John Wiley & Sons. 1992
