Maschinensemantik
Unter der Semantik einer Maschine versteht man das Zusammenspiel der operationellen Semantik mit der Ein- und Ausgabecodierung einer realen oder abstrakten Rechenmaschine, so dass sich das Ergebnis einer Berechnung zweifelsfrei bestimmen lässt. Sie stellt damit einen typischen Anwendungsfall für eine formale Semantik in der theoretischen Informatik dar und wird insbesondere für Korrektheitsbeweise bei der Analyse von Maschinen verwendet.
Die operationelle Semantik definiert, wie sich die Maschine zu einem gegebenen Zeitpunkt verhält, sie gibt also die schrittweise Verarbeitung von Daten mittels eines Programms vor. Wie dieses Programm aussieht und wie es in einzelne Arbeitsschritte umgesetzt wird, ist Teil der operationellen Semantik. Die Eingabecodierung legt fest, auf welche Weise die Maschine von außen Daten erhält und wie diese intern repräsentiert werden. Die Ausgabecodierung legt fest, welche Daten auf welche Weise zum Abschluss einer Berechnung als Ergebnis interpretiert werden sollen. Dies lässt sich folgendermaßen formalisieren:
Sei ein Programm, durch das im Rahmen des jeweiligen Maschinenmodells die schrittweise Verarbeitung von Eingabedaten aufgrund der operationellen Semantik der Maschine eindeutig festgelegt ist. Sei außerdem EC die Eingabecodierung und AC die Ausgabecodierung. Dann ist die Semantik der Maschine M eine Funktion mit
Beispiel: Das Programm der Maschine kann als Flussdiagramm oder Programmtext einer Programmiersprache angegeben sein. Es muss nun ein Startzustand definiert sein, in welchem der Maschine die Eingabedaten zugeführt werden. Je nach Maschinenmodell könnten diese Daten beispielsweise in ein spezielles Register (Registermaschine) oder auf ein spezielles Eingabeband (Turingmaschine) übertragen werden, so dass die Maschine nun mit der Abarbeitung des Flussdiagrammes oder Programmtextes beginnen und dabei auf diese Daten zugreifen kann. Durch die Abarbeitung des Flussdiagrammes geht die Maschine schließlich ggf. in einen Haltezustand über. Nun muss festgelegt sein, wie dieser Endzustand der Maschine im Sinne eines Rechenergebnisses zu interpretieren ist. Eine solche Interpretation kann etwa der Inhalt eines bestimmten Registers einer Registermaschine oder die Bandinschrift auf einer bestimmten Seite des Lese-/Schreibkopfes einer Turingmaschine sein.