Go backward to Operational PropertiesGo up to TopGo forward to Properties of Operational Semantics |

Op. semantics reduces programs to values.

- A program is a phrase [[C:
`comm`]]*s*._{0} - Values are from semantic domains.
- Booleans, numerals, locations, storage vectors.

- Equational definitions get rewrite rules.
- Denotation:
*f(x*_{1}, x_{2}, ..., x_{n}) = v - Rule:
*f(x*_{1}, x_{2}, ..., x_{n}) => v

- Denotation:
- Computation is a sequence of rewrite steps
*p*._{0}=>* p_{n}*p*._{0}=> p_{1}=> ...=> p_{n}- Each computation step
*p*replaces a subphrase (the redex) in_{i}=> p_{i+1}*p*according to some rewrite rule._{i}

- If
*p*is a value, computation terminates._{n}

*Which properties shall semantics fulfill?*

Author: Wolfgang Schreiner

Last Modification: March 26, 1998