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
- Computation is a sequence of rewrite steps p_0
=>* p_n.
- p_0
=> p_1
=> ...=> p_n.
- Each computation step p_i => p_{i+1} replaces
a subphrase (the redex) in p_i according to some rewrite rule.
- If p_n is a value, computation terminates.
Which properties shall semantics fulfill?
