Editing Operational semantics (section)

==== Structural operational semantics ====
'''Structural operational semantics''' (SOS, also called '''structured operational semantics''' or '''small-step semantics''') was introduced by [[Gordon Plotkin]] in ([[#plotkin81|Plotkin81]]) as a logical means to define 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 definition|inductive]], view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of) [[State transition system|transition relation]](s). SOS specifications take the form of a set of [[inference rule]]s that 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 [[#plotkin81|Plotkin81]] and [[#hennessybook|Hennessy90]], and other textbooks. Let <math>C_1, C_2</math> range over programs of the language, and let <math>s</math> range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by <math>E</math>), values {{nobreak|(<math>V</math>)}} and locations (<math>L</math>), then a memory update command would have semantics:

<math>
\frac{\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle\longrightarrow (s\uplus (L\mapsto V))}
</math>
<!-- NOTE: This is only a fragment of a full semantics. I've tried to include enough to illustrate the points but not so much that it takes a disproportionate amount of space.  -->

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

The semantics of sequencing can be given by the following three rules:

<math>
\frac{\langle C_1,s\rangle \longrightarrow s'}
{\langle C_1;C_2 \,,s\rangle\longrightarrow \langle C_2, s'\rangle}
\quad\quad
\frac{\langle C_1,s\rangle \longrightarrow \langle C_1',s'\rangle}
{\langle C_1;C_2 \,,s\rangle\longrightarrow \langle C_1';C_2\,, s'\rangle}
\quad\quad
\frac{}
{\langle \mathbf{skip} ,s\rangle\longrightarrow s}
</math>

Informally, the first rule says that,
if program <math>C_1</math> in state <math>s</math> finishes in state <math>s'</math>, then the program <math>C_1;C_2</math> in state <math>s</math> will reduce to the program <math>C_2</math> in state <math>s'</math>.
(You can think of this as formalizing "You can run <math>C_1</math>, and then run <math>C_2</math>
using the resulting memory store.)
The second rule says that
if the program <math>C_1</math> in state <math>s</math> can reduce to the program <math>C_1'</math> with state <math>s'</math>, then the program <math>C_1;C_2</math> in state <math>s</math> will reduce to the program <math>C_1';C_2</math> in state <math>s'</math>.
(You can think of this as formalizing the principle for an optimizing compiler:
"You are allowed to transform <math>C_1</math> as if it were stand-alone, even if it is just the
first part of a program.")
The semantics is structural, because the meaning of the sequential program <math>C_1;C_2</math>, is defined by the meaning of <math>C_1</math> and the meaning of <math>C_2</math>.

If we also have Boolean expressions over the state, ranged over by <math>B</math>, then we can define the semantics of the '''while''' command:
<math>
\frac{\langle B,s\rangle \Rightarrow \mathbf{true}}{\langle\mathbf{while}\ B\ \mathbf{ do }\ C,s\rangle\longrightarrow \langle C;\mathbf{while}\ B\ \mathbf{do}\ C,s\rangle}
\quad
\frac{\langle B,s\rangle \Rightarrow \mathbf{false}}{\langle\mathbf{while}\ B\ \mathbf{ do }\ C,s\rangle\longrightarrow s}
</math>

Such a definition allows formal analysis of the behavior of programs, permitting the study of [[Relation (mathematics)|relations]] between programs. Important relations include [[simulation preorder]]s and [[bisimulation]].
These are especially useful in the context of [[Concurrency (computer science)|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 ([[#plotkin81|Plotkin81]]) has attracted more than 1000 citations according to the CiteSeer [http://citeseer.ist.psu.edu/673965.html],
making it one of the most cited technical reports in [[Computer Science]].