Go backward to Soundness TheoremGo up to TopGo forward to Denotations as Rewrite Rules |

- 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`:=@_{3}`loc`+1:_{1}`comm`]]*(3, 4, 5)*

=>`update`(`loc`,_{3}

[[@`loc`+1:_{1}`intexp`]]*(3, 4, 5)*,*(3, 4, 5)*)

=> ...

=>`update`(`loc`, 4,_{3}*(3, 4, 5)*)

=>*(3, 4, 4)*

- [[

*Can we use denotational definitions as operational rewrite rules?*

Author: Wolfgang Schreiner

Last Modification: March 26, 1998