Go backward to
The Meaning of Identifiers
Go up to
Top
Go forward to
The Meaning of Identifiers
The Meaning of Identifiers
Valuation
I
:
Id -> Environment -> Store -> (Location × Storable-value)
L
: Id -> Environment -> Store -> Location.
R
: Id -> Environment -> Store -> Storable-value.
L
[[I]] =
accessenv
[[I]]
R
[[I]] =
access
o
accessenv
[[I]]
Semantic equations with variables
E
[[I]] =
R
[[I]]
C
[[I:=E]] =
lambda
e.
lambda
s.
return(
update
(
L
[[I]]e) (
E
[[E]]e s) s)
Author:
Wolfgang Schreiner
Last Modification: November 18, 1997