Operational semantics
270062
224557295
2008-07-09T11:56:18Z
Smrmousavi
7439260
/* References */
In [[computer science]], '''operational semantics''' is a way to give meaning to [[computer program]]s in a mathematically rigorous way (See [[formal semantics of programming languages]]).
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 program]]s, 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 [[Nondeterminism|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:
<blockquote>
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|Algol68]], Section 2)
</blockquote>
The first use of the word "operational semantics" in its present meaning is attributed to
Dana Scott ([[#plotkin04b|Plotkin04b]]).
What follows is a quote from Scott's seminal paper on formal semantics,
in which he mentions the "operational" aspects of semantics.
<blockquote>
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|Scott70]])
</blockquote>
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|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 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 which define the valid transitions of a composite piece of syntax
in terms of the transitions of its components.
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 ([[#plotkin04a|Plotkin04a]]) has attracted some 900 citations according to the CiteSeer [http://citeseer.ist.psu.edu/673965.html],
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 ==
* <cite id=plotkin04a> [[Gordon Plotkin | Gordon D. Plotkin.]] [http://citeseer.ist.psu.edu/673965.html 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) ([http://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf preprint]). </cite>
* <cite id=plotkin04b> [[Gordon Plotkin | Gordon D. Plotkin.]] The Origins of Structural Operational Semantics. JALP. 60-61:3-15, 2004. ([http://homepages.inf.ed.ac.uk/gdp/publications/Origins_SOS.pdf preprint]). </cite>
* <cite id=scott70> [[Dana Scott | Dana S. Scott.]] Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.</cite>
* <cite id=algol68> [[ Adriaan van Wijngaarden | Adriaan van Wijngaarden]] et. al. [[ALGOL 68 | Revised Report on the Algorithmic Language ALGOL 68. IFIP. 1968. ]] ([http://vestein.arb-phys.uni-dortmund.de/~wb/RR/rr.pdf])</cite>
[[Category:Formal specification languages]]
[[Category:Logic in computer science]]
[[Category:Semantics]]
[[de:Operationale Semantik]]
[[fr:Sémantique opérationnelle]]
[[hr:Operacijska semantika]]
[[ja:操作的意味論]]
[[pt:Semântica operacional]]