Go backward to Program Equivalence Go up to Top Go forward to Programs are Functions

Programs Are Functions

• Simplifications were operational-like.
• Answer computed from program and input.

Z:=1;

if A=0 then diverge;

Z:=3.

V P

lambdan.let s1 = ( [ [[A]] |-> n] newstore)

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

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

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

in access [[Z]] s'

Study denotation without sample input!