Programming Notes – Assignment Statement Theorems
In the axiom and theorems that follow r is the relation formed between the initial state and resulting state on the activation of the assignment statement ‘x := E’.
Axiom 1: s (x := E) t º t = {<’x’,E[s]>,<’y’,Sy>,×××,<’z’,Sz>}
s (x := E) t º t = {<’x’,E[s]>,(,i|1£i£m:<’t.i’,Ss.i>)}
Theorem 1: s (x := E) t Þ t Î R º s Î R[x := E]
(given s (x := E) t, prove LHS º RHS)
t Î R
º(Program State Part 1 Theorem 4)
R[t]
=(Axiom 1)
R[{<’x’,E[s]>,(,i|1£i£m:<’t.i’,Ss.i>)}]
=(Program State Part 1 Theorem 5)
R[{<’x’,E[s]>,(,i|1£i£m:<’t.i’,s.i[s]>)}]
=(corresponding variables are equal)
R[{<’x’,E[s]>,(,i|1£i£m:<’t.i’,t.i[s]>)}]
=(Program State Part 1 Theorem 1)
R[{<’x’,E>,(,i|1£i£m:<’t.i’,t.i>)}[s]]
=(Program State Part 1 Axiom 5)
R[{<’x’,E>,(,i|1£i£m:<’t.i’,t.i>)}][s]
=(Program State Part 1 Theorem 3)
R[x := E][s]
º(Program State Part 1 Theorem 4)
s Î R[x := E]
End of Proof
Corollary: s (x := E) t Ù s Î R[x := E] Þ t Î R
(Theorem 1)
s (x := E) t Þ t Î R º s Î R[x := E]
Þ(weakening of equivalence)
s (x := E) t Þ (s Î R[x := E]Þ t Î R)
º(shunting)
s (x := E) t Ù s Î R[x := E]Þ t Î R
End of Proof
Corollary: s (x := E) t Ù t Î R Þ s Î R[x := E]
(Theorem 1)
s (x := E) t Þ t Î R º s Î R[x := E]
Þ(weakening of equivalence)
s (x := E) t Þ (t Î R Þ s Î R[x := E])
º(shunting)
s (x := E) t Ù t Î R Þ s Î R[x := E]
End of Proof
Theorem 2: ran.(x := E).R[x :=E] Í R
(Í is reflexive)
ran.(x := E).R[x :=E] Í ran.’x := E’.R[x :=E]
º(definition of Í)
("t| t Î ran.(x := E).R[x :=E]: tÎran.’x := E’.R[x :=E])
("t| t Î ran.(x := E).R[x :=E]:
tÎ{b|($a|:a (x := E) b Ù a Î R[x :=E]):b})
º(definition of Î)
("t| t Î ran.(x := E).R[x :=E]:
($b|($a|:a (x := E) b Ù a Î R[x :=E]):b=t))
º(one point rule)
("t| t Î ran.(x := E).R[x :=E]:
($a|:a (x := E) t Ù a Î R[x :=E]))
Þ(Corollary to Theorem 1)
("t| t Î ran.(x := E).R[x :=E]:($a|: t Î R))
º(false Ú P ºP, distribute Ú over $)
("t| t Î ran.(x := E).R[x :=E]: t Î R Ú($a|: false))
º(trading, empty range, false Ú P ºP)
("t| t Î ran.(x := E).R[x :=E]: t Î R)
º(definition of Í)
ran.(x := E).R[x :=E] Í R
End of Proof
Theorem 3: (R[x :=E] Ç dom.(x := E)) {x := E} R
(Given S(x := E), the proof uses the concept (True Þ P) º P)
(Theorem 2)
ran.(x := E).R[x :=E] Í R
º(Weakest Liberal Precondition Theorem 1)
R[x :=E] Í WLP.(x := E).R
Þ(P Í Q Þ P Ç R Í Q Ç R)
R[x :=E] Ç dom.(x := E) Í WLP.(x := E).R Ç dom.(x := E)
º(Weakest Liberal Precondition Theorem 2)
R[x :=E] Ç dom.(x := E) Í WLP.(x := E).R Ç T.(x := E)
º(Weakest Precondition Axiom 1)
R[x :=E] Ç dom.(x := E) Í WP.(x := E).R
º(Weakest Precondition Axiom 2)
(R[x :=E] Ç dom.(x := E)) {x := E} R
End of Proof
Theorem 4: dom.(x := E) = U Þ R[x :=E] {x := E} R
(Given dom.(x := E) = U, prove that the Hoare triple is true.)
(Theorem 3)
(R[x :=E] Ç dom.(x := E)) {x := E} R
º(given)
(R[x :=E] ÇU) {x := E} R
º(identity of Ç)
R[x :=E] {x := E} R
End of Proof
Theorem 5: dom.(x := E).R Í R[x := E]
(Í is reflexive)
dom.(x := E).R Í dom.(x := E).R
º(definition of Í)
("s| sÎ dom.(x := E).R: s Î dom.(x := E).R)
("s| sÎ dom.(x := E).R:
sÎ{a|($b|:a (x := E) b Ù b Î R):a})
º(definition of Î)
("s| sÎ dom.(x := E).R:
($a|($b|:a (x := E) b Ù b Î R):a=s))
º(one point rule)
("s| sÎ dom.(x := E).R:
($b|:s (x := E) b Ù b Î R))
Þ(Corollary to Theorem 1)
("s| sÎ dom.(x := E).R:($b|: s Î R[x := E]))
º(false Ú P ºP, distribute Ú over $)
("s| s Î dpm.(x := E).R: s Î R[x := E] Ú($b|: false))
º(trading, empty range, false Ú P ºP)
("s| s Î ran.(x := E).R: s Î R[x := E])
º(definition of Í)
dom.(x := E).R Í R[x := E]
End of Proof
Theorem 6: R[x := E] Í dom.(x := E) Þ
R[x := E] Í dom.(x := E).R
(Given R[x := E] Í dom.(x := E), prove LHS Í RHS,
the proof uses the concept (True Þ P) º P)
(Theorem 2)
ran.(x := E).R[x :=E] Í R
dom.(x := E).(ran.(x := E).R[x :=E]) Í dom.(x := E).R
º(given, Relations Part 2 Theorem 15, identity of Ù)
R[x := E] Í dom.(x := E).(ran.(x := E).R[x := E]) Ù
dom.(x := E).(ran.(x := E).R[x :=E]) Í dom.(x := E).R
Þ(transitivity of Í)
R[x := E] Í dom.(x := E).R
End of Proof
Theorem 7: R[x := E] Í dom.(x := E) Þ R[x := E] = dom.(x := E).R
(Given R[x := E] Í dom.(x := E), prove LHS = RHS)
(given, Theorem 6)
R[x := E] Í dom.(x := E).R
º(Theorem 5, identity of Ù)
R[x := E] Í dom.(x := E).R Ù dom.(x := E).R Í R[x := E]
º(P Í Q Ù Q Í P º P = Q)
R[x := E] = dom.(x := E).R
End of Proof
Theorem 8: R[x := E] Í dom.(x := E) Þ R[x := E] = WP.(x := E).R
(Given R[x := E] Í dom.(x := E), prove RHS = LHS)
WP.(x := E).R
=(Weakest Precondition Theorem 6)
cond.(x := E).R
dom.(x := E).R – dom.(x := e).~R
=(given, Theorem 7)
R[x := E] - ~R[x := E]
=(A - ~A = A)
R[x := E]
End of Proof
Theorem 9: Given K is a constant of consistent type for Prog.x,
U {x := K} {State.s|: Prog.x = K}
(Given K is a constant of consistent type for Prog.x.
Then the dom.(x := K) = U)
(Theorem 4)
{State.s|: Prog.x = K}[x := k]
{x := K}
{State.s|: Prog.x = K}
º(substitution)
{State.s|: K = K} {x := K} {State.s|: Prog.x = K}
º(equality is reflexive)
{State.s|: true} {x := K} {State.s|: Prog.x = K}
º(Universal set)
U {x := K} {State.s|: Prog.x = K}
End of Proof
Theorem 10: Given K is a constant of consistent type for Prog.x,
WP.(x := K).{State.s|: Prog.x = K} = U
(Given K is a constant of consistent type for Prog.x)
WP.(x := K).{State.s|: Prog.x = K}
=(Theorem 8)
{State.s|: Prog.x = K}[x := K]
=(substitution)
{State.s|: K = K}
=(equality is reflexive)
{State.s|: true}
=(Universal set)
U
End of Proof
Theorem 11: E is a function over the weakest precondition Þ {x := E} is a function over the weakest precondition.
(given s Î WP.{x := E} Þ s {x := E} t Ù s {x := E} r, the variable x is represented by variable t.0, r.0,
prove that t = r)
(given, axiom 1)
t = {<’t.0’,E[s]>,(,i|1£i£m:<’t.i’,Ss.i>)}
º(Program State Part 1 Axiom 4)
Tt.0 = E[s] Ù ("i|i£1£m: Tt.i = Ss.i)
(given, axiom 1)
r = {<’r.0’,E[s]>,(,i|1£i£m:<’r.i’,Ss.i>)}
º(Program State Part 1 Axiom 4)
Rr.0 = E[s] Ù ("i|i£1£m: Rr.i = Ss.i)
º(combine expressions, Ù distributes over ")
Tt.0 = E[s] Ù Rr.0 = E[s] Ù ("i|i£1£m: Tt.i = Ss.i Ù Rr.i = Ss.i)
º(E is a function over the weakest precondition)
Tt.0 = Rr.0 Ù ("i|i£1£m: Tt.i = Ss.i Ù Rr.i = Ss.i)
º(= is transitive)
Tt.0 = Rr.0 Ù ("i|i£1£m: Tt.i = Rr.i)
º(Program State Part 1 Axiom 4)
t = r
End of Proof
References:
Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall
Fejer, Peter A., 1991, Mathematical foundations of computer science, New York, NY: Springer-Verlag
Gries, David, 1981, The Science of Programming, New York, NY: Springer-Verlag
Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag