Go backward to Expression Semantics Go up to Top Go forward to Soundness of the Typing Rules. |
P = Q; R
Q = loc2:=1;
R = if @loc2=0 then skip else S fi
S = loc1:=@loc2+4
[[P: comm]](s)
= [[R: comm]]([[Q: comm]](s))
= [[R: comm]]update(loc2, 1, s)
= if([[@loc2=0: boolexp]]update(loc2, 1,
s),
[[skip: comm]]update(loc2, 1,
s),
[[S: comm]]update(loc2, 1, s))
= if(false,
[[skip: comm]]update(loc2, 1,
s),
[[S: comm]]update(loc2, 1, s))
= [[S: comm]]update(loc2, 1, s)
= update(loc1,
[[@loc2+4:
intexp]]update(loc2, 1, s),
update(loc2, 1, s))
= update(loc1, 5, update(loc2, 1, s))
Program semantics can be studied independently of specific storage
vector!