Go backward to Operational Properties Go up to Top Go forward to Properties of Operational Semantics

Denotations as Rewrite Rules

Op. semantics reduces programs to values.

• A program is a phrase [[C: comm]]s₀.
• Values are from semantic domains.
  • Booleans, numerals, locations, storage vectors.
• Equational definitions get rewrite rules.
  • Denotation: f(x₁, x₂, ..., x_n) = v
  • Rule: f(x₁, x₂, ..., x_n) => v
• Computation is a sequence of rewrite steps p₀ =>* p_n.
  • p₀ => p₁ => ...=> 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?