Operational semantics
The operational semantics is a technique of computer science to the meaning or the semantics to describe computer programs. The effect of a program is understood as a step-by-step change of state of an abstract machine . Operational semantics are used to prove properties of individual programs or to relate programs to one another.
The concept of the program state is central to operational semantics . A status describes (in most cases) an assignment of the program variables and a position in the program. Furthermore, it is defined when and how conditions change. This is done either with the help of a state transition function or through so-called inference rules (i.e. rule-based). State transition functions or inference rules define an interpreter.
In order to work with the operational semantics of a program, a small piece of the original program is usually abstracted. An abstract program is set up which is equivalent to the original (the concrete program) and which can be executed by an abstract interpreter. The effects that this abstract program produces on the states of the abstract machine are then equivalent to the states that are obtained when the concrete program is executed.
A special case of operational semantics is Structured Operational Semantics (SOS), which was introduced by Gordon Plotkin .
Examples of the use of operational semantics are the semantic specifications of Algol 60 , PL / I or VDL .
In addition to operational semantics, there are also denotational semantics and axiomatic semantics to describe the semantics of computer programs.
literature
- Hanne Riis Nielson, Flemming Nielson: Semantics With Applications - A Formal Introduction, John Wiley & Sons. 1992