Programming Notes – Weakest Precondition

 

Axiom 1: WP.r.R = WLP.r.R Ç T.r

 

Definition 1: WP.r = WP.r.U

 

Axiom 2: P {r} R º P Í WP.r.R

 

Theorem 1: WP.r.R Í WLP.r.R

(Show LHS Í RHS)

      WP.r.R

=(Axiom 1)

      WLP.r.R Ç T.r

Í(A Ç B Í A)

      WLP.r.R

End of Proof

 

Theorem 2: P Í Q Þ WP.r.P Í WP.r.Q

(Show LHS Þ RHS)

      P Í Q

Þ(Weakest Liberal Precondition Theorem 3)

WLP.r.P Í WLP.r.Q

Þ(P Í Q Þ P Ç R Í Q Ç R)

WLP.r.P Ç T.r Í WLP.r.Q Ç T.r

º(Axiom 1)

WP.r.P Í WP.r.Q

End of Proof 

 

Corollary: WP.r.P Í WP.r.U

(Universal set U)

P Í U

Þ(Theorem 2)

      WP.r.P Í WP.r.U

End of Proof       

     

Theorem 3: WP.r.P Ç WP.r.Q = WP.r.(PÇQ)

(Weakest Liberal Precondition Theorem 4)

      WLP.r.P Ç WLP.r.Q = WLP.r.(PÇQ)

º(P = Q º P Ç R = Q Ç R)

      WLP.r.P Ç WLP.r.Q Ç T.r  = WLP.r.(PÇQ) Ç T.r

º(idempotency of Ç, symmetry of Ç)

      WLP.r.P Ç T.rÇ WLP.r.Q Ç T.r = WLP.r.(PÇQ) Ç T.r

º(Axiom 1)

      WP.r.P Ç WP.r.Q = WP.r.(PÇQ)

End of Proof

 

Theorem 4: WP.r.P È WP.r.Q Í WP.r.(PÈQ)

(Prove using (True Þ P) Þ P)

(Weakest Liberal Precondition Theorem 5)

(WLP.r.P È WLP.r.Q) Í WLP.r.(PÈQ)

Þ(P Í Q Þ P Ç R Í Q Ç R)

(WLP.r.P È WLP.r.Q)Ç T.rÍ WLP.r.(PÈQ)Ç T.r

º(Distribute Ç over È)

((WLP.r.P Ç  T.r) È (WLP.r.Q)Ç T.r))

Í WLP.r.(PÈQ)Ç T.r

º(Axiom 1)

(WP.r.P È WP.r.Q) Í WP.r.(PÈQ)

End of Proof

     

Theorem 5: ("X|:~WLP.r.X = WLP.r.~X) Þ WP.r.(RÈQ) = WP.r.R È WP.r.Q

(Given ~WLP.r.R = WLP.r.~R, prove LHS = RHS)

Þ(Given, Weakest Liberal Precondition Theorem 6)

WLP.r.(RÈQ) = WLP.r.R È WLP.r.Q)

º(P = Q º P Ç R = Q Ç R)

WLP.r.(RÈQ) Ç T.r= (WLP.r.R È WLP.r.Q)) Ç T.r

º(Distribute Ç over È)

WLP.r.(RÈQ) Ç T.r

= (WLP.r.R Ç T.r) È (WLP.r.Q Ç T.r)

º(Axiom 1)

WP.r.(RÈQ) = WP.r.R È WP.r.Q

End of Proof

 

Theorem 6: WP.r.R = cond.r.R

(show LHS = RHS)

(Axiom 1)

WP.r.R = WLP.r.R Ç T.r

º(given, Weakest Liberal Precondion Theorem 2)

WP.r.R = WLP.r.R Ç dom.r

º(Weakest Liberal Precondion Theorem 7)

WP.r.R = ~dom.r.(~R) Ç dom.r

º(Symmetry of Ç, definition of set difference)

WP.r.R = dom.r - dom.r.(~R)

º(Condition Theorem 2) 

WP.r.R = cond.r.R

End of Proof     

 

Theorem 7: WP.r.Æ = Æ

(Prove LHS = RHS)

      WP.r.Æ

=(Axiom 1)

WLP.r.ÆÇ T.r

=(PÍQºP=PÇQ, Weakest Liberal Precondion Theorem 9)

WLP.r.ÆÇ ~T.rÇ T.r

=(PÇ~P = Æ)

WLP.r.ÆÇÆ

=(PÇÆ = Æ)

Æ

End of Proof 

 

Theorem 8: WP.r.R Ç T.r = WP.r.R

(Axiom 1, A Ç B Í B)

      WP.r.R Í T.r

º(A Í B º A Ç B = A)

      WP.r.R Ç T.r = WP.r.R

End of Proof

 

Theorem 9: r is a function Þ WP.r.R = dom.r.R

(given r is a function, prove LHS = RHS)

      WP.r.R

=(given, Theorem 6)

      cond.r.R

=(Condition Theorem 7)

      dom.r.R

End of Proof

 

 

References:

 

Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall

 

Fejer, Peter and Simovici, Dan A., 1991, Mathematical Foundations of Computer Science, New York, NY: Springer-Verlag

 

Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag

 

Hu Sze-Tsen, 1963, Elements of Modern Algebra, San Francisco: Holden-Day, Inc.

 

Winskel, Glynn 1993 The Formal Semantics of Programming Languages: An Introduction, Cambridge, MA The MIT Press