Go backward to Expression Semantics Go up to Top Go forward to Soundness of the Typing Rules.

Example

P = Q; R
Q = loc₂:=1; R = if @loc₂=0 then skip else S fi
S = loc₁:=@loc₂+4

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