Go backward to Denotations as Rewrite Rules
Go up to Top
Go forward to Computability of Phrases
Properties of Operational Semantics
- Soundness.
- If p has an underlying "meaning" m and p
=> p', then p' means m as well.
- By definition of =>.
- Subject reduction.
- If p has an underlying "type" T and p
=> p', then p' has T as well.
- By soundness of typing.
- Strong typing.
- If p is well-typed and p
=> p', then p' contains no operator-operand
incompatibilities.
- By induction over computation rules.
- Computational adequacy.
- A program p's underlying meaning is a proper meaning m, if there is
some value v such that p => v and v means m.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine