The operational semantics for a programming language describes how a valid program 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.)

For the first time, the concept of operational semantics was used in defining the semantics of Algol 68. The following statement is a quote from the revised ALGOL 68 report:

The meaning of a program in the strict language is explained in terms of a hypothetical computer which performs the set of actions which constitute the elaboration of that program. (Algol68, Section 2)

The first use of the word "operational semantics" in its present meaning is attributed to Dana Scott (Plotkin04b). What follows is a quote from Scott's seminal paper on formal semantics, in which he mentions the "operational" aspects of semantics.

It is all very well to aim for a more ‘abstract’ and a ‘cleaner’ approach to semantics, but if the plan is to be any good, the operational aspects cannot be completely ignored. (Scott70)

Perhaps the first formal incarnation of operational semantics was that of the lambda calculus. Abstract machines in the tradition of the SECD machine are also closely related.

Structural Operational Semantics (SOS)

Structural Operational Semantics (SOS) was introduced by Gordon Plotkin in (Plotkin04a) as a logical means to defining operational semantics. The basic idea behind SOS is to define the behavior of a program in terms of the behavior of its parts, thus providing a structural, i.e., syntax oriented and inductive, view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of) transition relation(s). SOS specifications take the form of a set of inference rules which define the valid transitions of a composite piece of syntax in terms of the transitions of its components.

For a simple example, we consider part of the semantics of a simple programming language; proper illustrations are given in Plotkin04a and Hennessy90, and other textbooks. Let $C\_1,\; C\_2$ range over programs of the language, and let $s$ range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by $E$), values ($V$) and locations ($L$), then a memory update command would have semantics $frac\{langle\; E,srangle\; Rightarrow\; V\}\{langle\; L:=E,,,sranglelongrightarrow\; (suplus\; (Lmapsto\; V))\}$

Informally, the rule says that "if the expression $E$ in state $s$ reduces to value $V$, then the program $L:=E$ will update the state $s$ with the assignment $L=V$".

The semantics of sequencing can be given by the following rules $frac\{langle\; C\_1,srangle\; longrightarrow\; langle\; C\_1\text{'},s\text{'}rangle\}\; \{langle\; C\_1;C\_2\; ,,sranglelongrightarrow\; langle\; C\_1\text{'};C\_2,,\; s\text{'}rangle\}\; quad\; frac\{langle\; C\_1,srangle\; longrightarrow\; s\text{'}\}\; \{langle\; C\_1;C\_2\; ,,sranglelongrightarrow\; langle\; C\_2,\; s\text{'}rangle\}\; quad\; frac\{\}\; \{langle\; mathbf\{skip\}\; ,sranglelongrightarrow\; s\}$

Informally, the first rule says that, if the program $C\_1$ in state $s$ can reduce to the program $C\_1\text{'}$ with state $s\text{'}$, then the program $C\_1;C\_2$ in state $s$ will reduce to the program $C\_1\text{'};C\_2$. The second rule says that if program $C\_1$ in state $s$ finishes in state $s\text{'}$, then the program $C\_1;C\_2$ in state $s$ will reduce to the program $C\_2$ in state $s\text{'}$. The semantics is structural, because the meaning of the sequential program $C\_1;C\_2$, is defined by the meaning of $C\_1$ and the meaning of $C\_2$.

If we also have Boolean expressions over the state, ranged over by $B$, then we can define the semantics of the while command: $frac\{langle\; B,srangle\; Rightarrow\; mathbf\{true\}\}\{langlemathbf\{while\}\; B\; mathbf\{\; do\; \}\; C,sranglelongrightarrow\; langle\; C;mathbf\{while\}\; B\; mathbf\{do\}\; C,srangle\}\; quad\; frac\{langle\; B,srangle\; Rightarrow\; mathbf\{false\}\}\{langlemathbf\{while\}\; B\; mathbf\{\; do\; \}\; C,sranglelongrightarrow\; s\}$

Such a definition allows formal analysis of the behavior of programs, permitting the study of relations between programs. Important relations include simulation preorders and bisimulation. These are especially useful in the context of concurrency theory.

Thanks to its intuitive look and easy to follow structure, SOS has gained great popularity and has become a de facto standard in defining operational semantics. As a sign of success, the original report (so-called Aarhus report) on SOS (Plotkin04a) has attracted some 900 citations according to the CiteSeer , making it one of the most cited technical reports in Computer Science.

See also

• Algebraic semantics
• Axiomatic semantics
• Denotational semantics
• Formal semantics of programming languages

References

• Gordon D. Plotkin. A Structural Approach to Operational Semantics (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004) (preprint).
• Gordon D. Plotkin. The Origins of Structural Operational Semantics. JALP. 60-61:3-15, 2004. (preprint).
• Dana S. Scott. Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.
• Adriaan van Wijngaarden et al. Revised Report on the Algorithmic Language ALGOL 68. IFIP. 1968. ()
• Matthew Hennessy. Semantics of Programming Languages. Wiley, 1990. available online