Programming Notes – Program States, Part 1
Definition 1: Point s = {<’x’,Sx>,<’y’,Sy>,×××,<’z’,Sz>}
Point s = {i|0£i£m:<’s.i’, Ss.i>}
Definition 2: s is an arbitrary point º s = {<’x’,x>,<’y’,y>,×××,<’z’,z>}
º s = {i|0£i£m:<’s.i’,s.i>}
Definition 3: P[substitution 1][substitution 2] = (P[substitution 1])[substitution 2]
Axiom 2: Ss.k = s.k Ú (ØOccurs(s.k, P) Ú ("i|0£i£m Ù i¹k: ØOccurs(s.k, Ss.i) Ù ØOccurs(s.i, Ss.k)) Þ
P[s] = P[s.k := Ss.k][(,i|0£i£m Ù i¹k:s.i) := (,i|0£i£mÙi¹k:Ss.i)]
Axiom 3: {<’x’,Sx>,<’y’,Sy>,×××,<’z’,Sz>}[t]
= {<’x’,Sx[t]>,<’y’,Sy[t]>,×××,<’z’,Sz[t]>}
{i|0£i£m:<’s.i’, Ss.i>}[t] = {i|0£i£m:<’s.i’, Ss.i[t]>}
Axiom 4: p=s º ("i|0£i£m:Ss.i = Pp.i)
Axiom 5: P[t[s]] = P[t][s]
Theorem 1: s[t] = {i|0£i£m:<’s.i’,Ss.i[t]>}
(Prove LHS º RHS)
s[t]
º(Definition 1)
{i|0£i£m:<’s.i’,Ss.i>}[t]
º(Axiom 3)
{i|0£i£m:<’s.i’,Ss.i[t]>}
End of Proof
Theorem 2: s is an arbitrary point Þ P = P[s]
(From Axiom 1 and s is arbitrary, P[s] = P[(,i|0£i£m:s.i) := (,i|0£i£m:s.i)]
prove by induction P[(,i|0£i£m:s.i) := (,i|0£i£m:s.i)] = P for all m)
Part 1: prove for m < 0
P[(,i|0£i£m:s.i) := (,i|0£i£m:s.i)]
=(m<0, algebra)
P[(,i|false:s.i) := (,i|false:s.i)]
=(empty range)
=(m<0, algebra)
P
End of Part 1 Proof
Part 2: Suppose true for m=n, prove for m=n+1)
P[(,i|0£i£n+1:s.i) := (,i|0£i£n+1:s.i)]
=(Axiom 2)
P[s.(n+1) := s.(n+1)][(,i|0£i£n:s.i) := (,i|0£i£n:s.i)]
=(definition 3, P[x := x] = P)
P[(,i|0£i£n:s.i) := (,i|0£i£n:s.i)]
=(true for m=n)
P
End of Part 2 Proof
End of Proof
Theorem 3: P[<’x’,E>,(,i|1£i£m:<’s.i’,s.i>)] = P[x := E]
(Prove by induction)
Part 1: Prove for m=0
P[<’x’,E>,(,i|1£i£0:<’s.i’,s.i>)]
=(axiom 1)
P[x,(,i|1£i£0:s.i) := E,(,i|1£i£0:s.i)]
=(algebra)
P[x,(,i|false:s.i) := E,(,i|false:s.i)]
=(empty range)
P[x := E]
End of Part 1 Proof
Part 2: Given true for m=n, prove true for m=n+1
P[<’x’,E>,(,i|1£i£n+1:<’s.i’,s.i>)]
=(Axiom 1)
P[x,(,i|1£i£n+1:s.i) := E,(,i|1£i£n+1:s.i)]
=(axiom 2)
P[s.(n+1} := s.{n+1}][x,(,i|1£i£n:s.i) := E,(,i|1£i£n:s.i)]
=(P[x := x] = P, definition 3)
P[x,(,i|1£i£n:s.i) := E,(,i|1£i£n:s.i)]
=(given)
P[x := E]
End of Part 2 Proof
End of Proof
Theorem 4: s Î P º P[s]
(prove LHS º RHS)
s Î P
º(definition of P)
s Î {x|P:x}
º(definition of Î)
($x|P:x=s)
º(x is arbitrary, Theorem 2)
($x|P[x]:x=s)
º(one point rule)
P[s]
End of Proof
Theorem 5: Let x be a program variable.
x[t] = Tx
(Let x be the variable t.m, Prove that
x[(,i|k£i£m:t.i) := (,i|k£i£m:Tt.i)] = Tx
for all 0£k£m. Prove by induction)
Part 1: Prove for k=m
x[(,i|m£i£m:t.i) := (,i|m£i£m:Tt.i)]
=(algebra)
x[(,i|m=i:t.i) := (,i|m=i:Tt.i)]
=(one point rule)
x[t.m := Tt.m]
=(given x = t.m)
x[x := Tx]
=(evaluate)
Tx
End of Part 1 Proof
Part 2: Given true for k=n<m, prove for k=n-1
x[(,i|n-1£i£m:t.i) := (,i|n-1£i£m:Tt.i)]
=(n<mÞØOccurs(t.n-1,x), Axiom 2)
x[t.(n-1) := Tt.(n-1)][(,i|n£i£m:t.i) := (,i|n£i£m:Tt.i)]
=(ØOccurs(x,P) Þ P[x := Q] = P)
x[(,i|n£i£m:t.i) := (,i|n£i£m:Tt.i)]
=(given)
Tx
End of Part 2 Proof
End of Proof
Theorem 6: Let t be a point, and let s be an arbitrary point.
t[s] = t
t[s]
=(Theorem 2, s is arbitrary)
t
Theorem 7: Let t be a point, and let s be an arbitrary point.
s[t] = t
s[t]
=(Theorem 1)
{i|0£i£m:<’s.i’,Ss.i[t]>}
=(s is arbitrary)
{i|0£i£m:<’s.i’,s.i[t]>}
=(Theorem 5)
{i|0£i£m:<’s.i’,Tt.i>}
=(corresponding variables are equal)
{i|0£i£m:<’t.i’,Tt.i>}
=(Definition 1)
t
End of Proof
(º is reflexive)
("s|:xÎU º xÎU)
º(membership of Universal set)
("s|:xÎU º true)
º(Constant at any point = constant)
("s|:xÎU º true[s])
º(Theorem 4)
("s|:xÎU º s Î {s|true:s))
º(Set equality)
U = {s|true:s)
End of Proof
Theorem 9: Æ = {s|false:s}
(º is reflexive)
("s|:xÎƺ xÎÆ)
º(membership of Null set)
("s|:x뮼 false)
º(Constant at any point = constant)
("s|:x뮼 false[s])
º(Theorem 5)
("s|:xÎƺ s Î {s|false:s))
º(Set equality)
Æ = {s|false:s)
End of Proof
References:
Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall
Ganong, Rick 1999, Course notes and comments from M1090 and M2090 math and logic courses, http://www.math.yorku.ca/Who/Faculty/Ganong
Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag
Winskel, Glynn 1993 The Formal Semantics of Programming Languages: An Introduction, Cambridge, MA The MIT Press