Programming Notes – skip Statement  

 

 

Axiom 1: a skip b º a = b

 

Theorem 1: dom.skip.R = R

(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

 

Theorem 2: cond.skip.R = R

(definition of cond)

      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

 

Theorem 3: R {skip} R

(Program Statement Solution Theorem 2)

      cond.skip.R {skip} R

º(Theorem 2)

      R {skip} R

End of Proof

 

Theorem 4: WP.skip.R = R

(Theorem 2)

      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})

º(Program Sequence Theorem 5)

     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

º(Program Sequence Theorem 5)

     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})

º(Program Sequence Theorem 5)

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

º(Program Sequence Theorem 5)

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

 

Theorem 13: ran.skip.P = P

(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

 

Theorem 14: SR.skip.P = P

(Proof uses True Þ P º P)

(Theorem 3)

      P {skip} P

Þ(Strongest Result Theorem 5)

      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