P = Q; R
Q = loc_2:=1;
R = if @loc_2=0 then skip else S fi
S = loc_1:=@loc_2+4
[[P: comm]](s)
= [[R: comm]]([[Q: comm]](s))
= [[R: comm]]update(loc_2, 1, s)
= if([[@loc_2=0: boolexp]]update(loc_2, 1,
s),
[[skip: comm]]update(loc_2, 1,
s),
[[S: comm]]update(loc_2, 1, s))
= if(false,
[[skip: comm]]update(loc_2, 1,
s),
[[S: comm]]update(loc_2, 1, s))
= [[S: comm]]update(loc_2, 1, s)
= update(loc_1,
[[@loc_2+4:
intexp]]update(loc_2, 1, s),
update(loc_2, 1, s))
= update(loc_1, 5, update(loc_2, 1, s))
Program semantics can be studied independently of specific storage vector!