Go backward to Soundness Theorem Go up to Top Go forward to Denotations as Rewrite Rules

Operational Properties

• Denotational semantics constructs mathematical functions.
  • Function extensionality for reasoning.
• Operational semantics reveals computational patterns.
  • Computation steps undertaken for evaluating the program.
• Denotational semantics has operational flower.
  • [[loc₃:=@loc₁+1: comm]](3, 4, 5)
    => update(loc₃,
        [[@loc₁+1: intexp]](3, 4, 5), (3, 4, 5))
    => ...
    => update(loc₃, 4, (3, 4, 5))
    => (3, 4, 4)

Can we use denotational definitions as operational rewrite rules?