SchrittSemantik

SchrittSemantik, im Deutschen oft als klein- oder kleinschrittige Semantik bezeichnet, ist ein Ansatz der formalen Semantik von Programmiersprachen. Sie beschreibt die Ausführung eines Programms als Folge von einzelnen, diskreten Schritten, wobei jeder Schritt eine minimale Änderung des Ausführungskontexts bewirkt. Eine Konfiguration besteht üblicherweise aus einem Ausdruck, einer Umgebung bzw. einem Speicherzustand und gegebenenfalls einem Steuerzustand. Die Semantik definiert eine Transitionsrelation →, die angibt, wie sich eine Konfiguration in eine Folge von Konfigurationen überführt, bis ein Wert oder eine Abbruchbedingung erreicht wird. Im Gegensatz dazu beschreibt die Big-Step-Semantik (natürliche Semantik) die Ausführung direkt vom Ausgangsausdruck zu einem Endwert in wenigen großen Schritten.

Typische Darstellungen der SchrittSemantik nutzen Inferenzregeln oder Transitionsregeln sowie Evaluation Contexts, um festzulegen, wo der nächste Schritt erfolgt. Beispiele in einer einfachen Ausdruckssprache: Falls e1 → e1', dann gilt auch e1 + e2 → e1' + e2 (Schrittregel für den linken Operand). Falls e1 ein Wert ist und e2 → e2', dann gilt auch v1 + e2' → v1 + e2'. Wenn beide Operanden numerisch sind, wird n1 + n2 direkt zu n3 reduziert, dem Summenwert. Durch solche Regeln entsteht eine explizite, ortsbezogene Reduktionsfolge, die die Ausführung schrittweise modelliert.

Anwendungen der SchrittSemantik liegen in der formalen Definition von Programmiersprachen, der Begründung von Korrektheit von Interpreter- oder Compiler-Algorithmen sowie in der Modellierung von Sprachen mit komplexem Kontrollfluss, Ausnahmen oder Nebenläufigkeit. Die Methode ist eng mit dem Konzept der Strukturellen Operational Semantik (SOS) verbunden und wird oft als Gegenstück zur Big-Step-Semantik betrachtet. Sie ermöglicht präzises Beweisen über Terminierung, Divergenz und Nichtdeterminismus sowie über andere Semantik-Eigenschaften.