Programming Notes – skip Statement
Axiom 1: a skip b º a = b
(Reflexive property of =)
dom.skip.R = dom.skip.R
º(definition of =)
("x|:x Î dom.skip.R º x Î dom.skip.R)
º(definition of dom.skip.R)
("x|:x Î dom.skip.R º x Î {a|($b|:a skip b Ù b Î R):a})
º(definition of Î)
("x|:x Î dom.skip.R º ($a|($b|:a skip b Ù b Î R):a=x))
º(One Point Rule)
("x|:x Î dom.skip.R º ($b|:x skip b Ù b Î R))
º(Axiom 1)
("x|:x Î dom.skip.R º ($b|:x = b Ù b Î R))
º(trading)
("x|:x Î dom.skip.R º ($b|x = b: b Î R))
º(One Point Rule)
("x|:x Î dom.skip.R º x Î R)
º(definition of =)
dom.skip.R = R
End of Proof
cond.skip.R = dom.skip.R – dom.skip.~R
º(Theorem 1)
cond.skip.R = R – ~R
º(A - ~A = A)
cond.skip.R = R
End of Proof
(Program Statement Solution Theorem 2)
cond.skip.R {skip} R
º(Theorem 2)
R {skip} R
End of Proof
cond.skip.R = R
º(Program State Part 4 Theorem 6)
WP.skip.R = R
End of Proof
Theorem 5: (Left Identity) WP.(skip;r).R = WP.r.R
(Prove LHS = RHS)
WP.(skip;r).R
=(Statement Sequence Theorem 2)
WP.skip.(WP.r.R)
=(Theorem 4)
WP.r.R
End of Proof
Corollary: P {skip;r} R º P {r} R
(Use (True Þ P) º P in proof)
(Theorem 5)
WP.(skip;r).R = WP.r.R
Þ(Corollary to Program Solutions Theorem 12)
P {skip;r} R º P {r} R
End of Proof
Theorem 6: (Right Identity) WP.(r;skip).R = WP.r.R
(prove LHS = RHS)
WP.(r;skip).R
=(Statement Sequence Theorem 2)
WP.r.(WP.skip.R)
=(Theorem 4)
WP.r.R
End of Proof
Corollary: P {r;skip} R º P {r} R
(Use (True Þ P) º P in proof)
(Theorem 6)
WP.(r;skip).R = WP.r.R
Þ(Corollary to Program Solutions Theorem 12)
P {r;skip} R º P {r} R
End of Proof
Theorem 7: Given K is a properly typed constant Ù Øoccurs(x,R),
P {x := K} (RÇ{State.s|:x=K}) º P {skip} R
(Given K is a properly typed constant ÙØoccurs(x,R), prove LHS º RHS)
P {x := K} (RÇ{State.s|:x=K})
º(Corollary to Theorem 5: Left Identity)
P {skip;x := K} (RÇ{State.s|:x=K})
P {skip} WP.(x := K).(RÇ{State.s|:x=K})
º(Weakest Precondition Theorem 3)
P {skip} (WP.(x := K).RÇ WP.(x := K).{State.s|:x=K})
º(Given, Assignment Statement Theorem 10)
P {skip} (WP.(x := K).RÇ U)
º(Identity of Ç)
P {skip} WP.(x := K).R
º(Given, Assignment Statement Theorem 8)
P {skip} R[x := K]
º(Given, Replacement rules)
P {skip} R
End of Proof
Theorem 8: Given K is a properly typed constant Ù Øoccurs(x,R),
P {x := K} R º P {skip} R
(Given K is a properly typed constant ÙØoccurs(x,R), prove LHS º RHS)
P {x := K} R
º(Corollary to Theorem 5: Left Identity)
P {skip;x := K} R
P {skip} WP.(x := K).R
º(Given, Assignment Statement Theorem 8)
P {skip} R[x := K]
º(Given, Replacement rules)
P {skip} R
End of Proof
Theorem 9: P {r} WP.s.R º P {skip} WP.s.R º P {r;s} R º P {s} R
(Prove LHS º RHS)
P {r} WP.s.R º P {skip} WP.s.R
º(Statement Sequence Theorem 9)
P {r;s} R º P {skip;s} R
º(Corollary to Theorem 5)
P {r;s} R º P {s} R
End of Proof
Theorem 10: WP.s.R = WP.skip.R Þ P {r;s} R º P {r} R
(Prove LHS Þ RHS)
WP.s.R = WP.skip.R
Þ(Statement Sequence Theorem 10)
P {r;s} R º P {r;skip) R
º(Corollary to Theorem 6)
P {r;s} R º P {r} R
End of Proof
Theorem 11: Given J,K is a properly typed constants Ù Øoccurs(x,R) ÙØoccurs(y,R),
P {x := J;y :=K} (RÇ{State.s|:x=J} Ç{State.s|:y=K}) º P {skip} R
(Prove LHS º RHS)
P {x:=J;y:=K} (RÇ{State.s|:x=J} Ç{State.s|:y=K})
P {x:=J} WP.(y:=K).(RÇ{State.s|:x=J} Ç{State.s|:y=K})
º(Weakest Precondition Theorem 3)
P {x:=J} WP.(y:=K).(RÇ{State.s|:x=J}) Ç WP.(y:=K).{State.s|:y=K})
º(Given, Assignment Statement Theorem 10)
P {x:=J} WP.(y:=K).(RÇ{State.s|:x=J}) ÇU
º(Identity of Ç)
P {x:=J} WP.(y:=K).(RÇ{State.s|:x=J})
º(Given, Assignment Statement Theorem 8)
P {x:=J} (RÇ{State.s|:x=J})[y := K]
º(Given, Replacement rules)
P {x:=J} RÇ{State.s|:x=J}
º(Given, Theorem 7)
P {skip} R
End of Proof
Theorem 12: Given J,K is a properly typed constants Ù Øoccurs(x,R) ÙØoccurs(y,R),
P {x := J;y :=K} R º P {skip} R
(Prove LHS º RHS)
P {x:=J;y:=K} R
P {x:=J} WP.(y:=K).R
º(Given, Assignment Statement Theorem 8)
P {x:=J} R[y := K]
º(Given, Replacement rules)
P {x:=J} R
º(Given, Theorem 8)
P {skip} R
End of Proof
(Reflexive property of =)
ran.skip.P = ran.skip.P
º(definition of =)
("y|:y Î ran.skip.P º y Î ran.skip.P)
º(definition of ran.skip.P)
("y|:y Î ran.skip.P º y Î {b|($a|:a skip b Ù a Î P):b})
º(definition of Î)
("y|:y Î ran.skip.P º ($b|($a|:a skip b Ù a Î P):b=y))
º(One Point Rule)
("y|:y Î ran.skip.P º ($a|:a skip y Ù a Î P))
º(Axiom 1)
("y|:y Î ran.skip.P º ($a|:a = y Ù a Î P))
º(trading)
("y|:y Î ran.skip.P º ($a|a = y: a Î P))
º(One Point Rule)
("y|:y Î ran.skip.P º y Î P)
º(definition of =)
ran.skip.P = P
End of Proof
(Proof uses True Þ P º P)
(Theorem 3)
P {skip} P
SR.skip.P = ran.skip.P
º(Theorem 13)
SR.skip.P = P
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