## [Operationale Semantik](/de/node/59559) Definition 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 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 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 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 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 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 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 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 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.