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
.
Author:
Wolfgang Schreiner
Last Modification: March 26, 1998