Go backward to Simplification Go up to Top Go forward to Simplification II

Program Denotation

Program plus input -> result.

Z:=1;

if A=0 then diverge;

Z:=3.

V P (two)

let s1 = ( [ [[A]] |-> two] newstore)

s2 = [ [[Z]] |-> one ]s1

s3 = ((access [[A]] s2) equals zero) -> _|_ [] s2

s' = [ [[Z]] |-> three ]s3

in access [[Z]] s'

||

three

Intermediate form (only partial simplification) delivers more insight!