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_3:=@loc_1+1:
comm]](3, 4, 5)
=> update(loc_3,
[[@loc_1+1:
intexp]](3, 4, 5),
(3, 4, 5))
=> ...
=> update(loc_3, 4,
(3, 4, 5))
=> (3, 4,
4)
Can we use denotational definitions as operational rewrite rules?
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine