Ein formales System, das die Bedeutung einer Programmiersprache durch Inferenzregeln definiert, welche beschreiben, wie Programmkonstrukte Ausführungszustände ändern oder zu Werten ausgewertet werden, üblicherweise in klein-Schritt-(Transitions-) oder groß-Schritt-(Evaluations-)Stilen dargestellt.

Prinzip

Die Programmbedeutung wird durch konkrete zustandsverändernde Regeln erfasst: Jeder syntaktischen Konstruktion werden Übergangs- oder Evaluationsregeln zugewiesen, die bestimmen, wie Laufzeitzustände sich entwickeln oder wie Ausdrücke Werte liefern.

Demonstration

Klein-Schritt-Beispiel: eine Relation s -> s', die einen arithmetischen Ausdruck reduziert (z. B. (1+2) → 3) oder eine Zuweisung, die einen Speicher aktualisiert (⟨x:=e,σ⟩ → ⟨skip,σ[x↦v]⟩ wenn e zu v auswertet). Groß-Schritt-Beispiel: ein Evaluationsurteil ⟨e,σ⟩ ⇓ v, das Ausdruck und Umgebung direkt einem Wert zuordnet (z. B. ⟨1+2,σ⟩ ⇓ 3).

Fehlanwendung

Die operationellen Regeln als Implementierungs-Timings interpretieren (aus abstrakten Schritten Laufzeit ableiten) oder Klein-Schritt-Regeln verwenden, ohne nichtdeterministische externe Interaktionen zu modellieren, und daraus Aussagen über beobachtbares I/O treffen; operationelle Semantik fälschlich mit den Beweisen deontologischer (denotationaler) Äquivalenz gleichsetzen, ohne formalen Zusammenhang herzustellen.

Konsequenz

Ermöglicht eine präzise, mechanisierbare Beschreibung des Laufzeitverhaltens, nützlich zum Beweisen von Eigenschaften wie Typsicherheit, Korrektheit von Compilertransformationen (durch Simulations- bzw. Schritt-Korrespondenz) und zum Ableiten von Interpreter-Implementierungen direkt aus den Regeln.

Umkehrung

Ersetze die schrittweise operationelle Beschreibung durch eine axiomatische oder denotationelle Darstellung: Die axiomatische Semantik liefert Beweisregeln über Assertions (Hoare-Dreiecke) ohne Ausführungsschritte; die denotationelle Semantik ordnet Programmphrasen mathematische Objekte zu statt Zustandsübergängen.

Abgrenzung

Umfasst formale Beschreibungen von Sprachkonstrukten, abstrakten Maschinen und Evaluationsrelationen. Modelliert nicht von sich aus Ressourcenverbrauch (Echtzeit/Energie), außer nach Erweiterung, und ersetzt nicht die empirischen Implementierungsfragen; schließt informelle, nicht-formalisierte Beschreibungen aus.

Semantische Spannung

Spannung gegenüber den denotationellen und axiomatischen Ansätzen: operationelle Semantik betont konkrete Berechnungsschritte, während die anderen abstrakte mathematische Bedeutung bzw. Korrektheits-Assertions fokussieren.

Synthese

Operationale Semantik ist das regelbasierte, schrittweise Formalismus, das Programmausführung explizit macht: Indem es angibt, wie jede Konstruktion Zustände transformiert oder in Werte evaluiert, bietet es eine mechanisierbare Grundlage zum Reasoning über Ausführung, zum Beweisen von Transformationen und zum Konstruieren von Interpretern, wobei Beobachtungs- und Ressourcenmodelle gezielt hinzugefügt werden können.