Operational semantics
From Wikipedia, the free encyclopedia
In computer science, operational semantics is a way to give meaning to computer programs 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 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.)
A common way to rigorously define the operational semantics, pioneered by Gordon Plotkin in his 1981 paper "A Structural Approach to 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 especially useful in the context of concurrency.
Defining operational semantics through a state transition system is usually done by giving an inductive definition of the set of possible transitions. This usually takes the form of a set of inference rules which define the valid transitions in the system.
The first operational semantics was that of the lambda calculus. Abstract machines in the tradition of the SECD machine are closely related.
[edit] See also
- Algebraic semantics
- Axiomatic semantics
- Denotational semantics
- Formal semantics of programming languages
[edit] 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).
