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.
- [[loc3:=@loc1+1:
comm]](3, 4, 5)
=> update(loc3,
[[@loc1+1:
intexp]](3, 4, 5),
(3, 4, 5))
=> ...
=> update(loc3, 4,
(3, 4, 5))
=> (3, 4,
4)
Can we use denotational definitions as operational rewrite rules?
Author: Wolfgang Schreiner
Last Modification: March 26, 1998