Content deleted Content added
Line 39:
'''Structural operational semantics''' (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>
| |||