Operational semantics

In computer science, operational semantics is one of the approaches to give meaning to computer programs in a mathematically rigorous way (see semantics of programming languages).

An operational semantics for a particular programming language describes how any particular valid program in the language is interpreted as sequences of computational steps. These sequences then are the meaning of the program. In the context of functional programs, the final step in a terminating sequence returns the value of the program. (In general there can be many computation sequences and many return values for a single program, because the program could be nondeterministic.)

One of the most common ways used to rigorously define an operational semantics is to provide a state transition system for the language of interest. Such a definition allows a formal analysis of a language, permitting the study of relations between programs. Important relations include simulation preorders and bisimulation. These are specially useful in the context of concurrency.

Defining an operational semantics through a state transition system is usually done by giving an inductive definition of the set of possible transtions. This usually takes the form of a set of inference rules which define the valid transitions in the system.

Operational semantics is related to denotational semantics through the concept of full abstraction.