Programming Notes – Programming Solutions Part 1

 

Definition 1: cond.r.R = dom.r.R – dom.r.~R

 

Theorem 1: WP.r.R {r} R

(Reflexive Property of Í)

WP.r.R Í WP.r.R

º(Weakest Precondition Axiom 2)

      WP.r.R {r} R

End of Proof

 

Theorem 2: cond.r.R {r} R

(Weakest Precondition Theorem 6)

      WP.r.R = cond.r.R

Þ(A = B Þ B Í A)

      cond.r.R Í WP.r.R

º(Weakest Preconditon Axiom 2)

      cond.r.R {r} R

End of Proof

 

Theorem 3: r is a function Þ dom.r.R {r} R

(Given r is a function, prove S(r) Þ dom.r.R {r} R)

(Theorem 2)

      cond.r.R {r} R

º(Given, Relation Condition Theorem 7)

      dom.r.R {r} R

End of Proof

 

Theorem 4: (dom.r.R Ç dom.r.~R = Æ) Þ dom.r.R {r} R

(Given dom.r.R Ç dom.r.~R = Æ, prove dom.r.R {r} R)

(Theorem 2)

      cond.r.R {r} R

º(given, Relation Condition Theorem 8)

dom.r.R {r} R

End of Proof

 

Theorem 5: R Í S Þ (P {r} R Þ P {r} S)

(given R Í S, show LHS Þ RHS)

      P {r} R

º(Weakest Precondition Axiom 2)

      P Í WP.r.R

º(Given, Weakest Precondition Theorem 2, identity of Ù)

      P Í WP.r.R Ù (WP.r.R Í WP.r.S)

Þ(transitivity of Í)

      P Í WP.r.S

º(Weakest Precondition Axiom 2)

      P {r} S

End of Proof

 

Corollary: (R Í S Ù P r R) Þ P {r} S

(Theorem 5)

R Í S Þ (P {r} R Þ P {r} S)

º(shunting)

(R Í S Ù P {r} R) Þ P {r} S

End of Proof

 

 

Theorem 6: P Í Q Þ (Q {r} R Þ P {r} R)

(given P Í Q, show LHS Þ RHS)

      Q {r} R

º(Weakest Precondition Axiom 2)

      Q Í WP.r.R

º(Given, identity of Ù)

      P Í Q Ù Q Í WP.r.R

Þ(transitivity of Í)

      P Í WP.r.R

º(Weakest Precondition Axiom 2)

      P {r} R

End of Proof

 

Corollary: (P Í Q Ù Q {r} R) Þ P {r} R

(Theorem 6)

P Í Q Þ (Q {r} R Þ P {r} R)

º(shunting)

(P Í Q Ù Q {r} R) Þ P {r} R

End of Proof

 

 

Theorem 7: P {r} R Ù Q {r} S Þ (PÇQ) {r} (RÇS)

(prove LHS Þ RHS)

      P {r} R Ù Q {r} S    

º(Program State Part 4 Axiom 2)

      P Í WP.r.R Ù Q Í WP.r.S

Þ(monotonicity of Ç)

      (PÇQ) Í (WP.r.R Ç WP.r.S)

º(Weakest Precondition Theorem 3)

      (PÇQ) Í WP.r.(RÇS)

º(Weakest Precondition Axiom 2)

      (PÇQ) {r} (RÇS)

End of Proof

 

Theorem 8: P {r} R Ù Q {r} S Þ (PÈQ) {r} (RÈS)

(prove LHS Þ RHS)

      P {r} R Ù Q {r} S    

º(Weakest Precondition Axiom 2)

      P Í WP.r.R Ù Q Í WP.r.S

Þ(monotonicity of È)

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

º(Weakest Precondition Theorem 4)

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

º(Weakest Precondition Axiom 2)

      (PÈQ) {r} (RÈS)

End of Proof

 

Theorem 9: P {r} R Ù P {r} S º P {r} (RÇS)

(Use ((PÞQ) Ù (QÞP)) º PºQ)

 

Part 1 Prove P {r} R Ù P {r} S Þ P {r} (RÇS)

      P {r} R Ù P {r} S

Þ(Theorem 7)

(PÇP) {r} (RÇS)

º(Idempotence of Ç

P {r} (RÇS)

End of Part 1 Proof

 

Part 2 Prove P {r} (RÇS) Þ P {r} R Ù P {r} S

P {r} (RÇS)

Þ(RÇSÍR, Theorem 5)

      P {r} R

Þ(RÇSÍS, Theorem 5, identity of Ù)

      P {r} R Ù P {r} S

End of Part 2 Proof

End of Proof

 

Theorem 10: P {r} R Ù Q {r} R º (PÈQ) {r} R

(Use ((PÞQ) Ù (QÞP)) º PºQ)

Part 1 Prove P r R Ù Q r R Þ (PÈQ) r R

      P {r} R Ù Q {r} R

Þ(Theorem 8)

(PÈQ) {r} (RÈR)

º(Idempotence of È

(PÈQ) {r} R

End of Part 1 Proof

 

Part 2 Prove (PÈQ) {r} R Þ P {r} R Ù Q {r} R

(PÈQ) {r} R

Þ(PÍPÈQ, Theorem 6)

      P {r} R

Þ(QÍPÈQ, Theorem 6, identity of Ù)

      P {r} R Ù Q {r} R

End of Part 2 Proof

End of Proof

 

Theorem 11: B Í WLP.r.R Þ (B Ç T.r) {r} R

(prove LHS Þ RHS)

      B Í WLP.r.R

º(Í is reflexive, identity of Ù)

      B Í WLP.r.R Ù T.rÍ T.r

Þ(Ç is monotonic)

      B Ç T.rÍ WLP.r.R Ç T.r

º(Weakest Precondition Axiom 1)    

      B Ç T.rÍ WP.r.R

º(Weakest Precondition Axiom 2)    

      (B Ç T.r) {r} R

End of Proof     

 

Theorem 12: WP.r.R = WP.s.R º ("A|A {r} R º A {s} R:A)

(Prove LHS Þ RHS Ù RHS Þ LHS)

 

Part 1
(Given WP.r.R = WP.s.R, prove ("A|A {r} R º A {s} R:A))

(º is reflexive)

      ("A|A {r} R º A {r} R:A)

º(Weakest Precondition Axiom 2) 

      ("A|A {r} R º A Í WP.r.R:A)

º(Given)

      ("A|A {r} R º A Í WP.s.R:A)

º(Weakest Precondition  Axiom 2) 

      ("A|A {r} R º A {s} R:A)

End of Part 1 Proof

 

Part 2
(Given ("A|A {r} R º A {s} R:A), prove WP.r.R = WP.s.R)

(instance of given)

      WP.r.R {r} R º WP.r.R {s} R

º(instance of given, identity of Ù)

      WP.r.R r R º WP.r.R {s} R Ù WP.s.R {r} R º WP.s.R s R

º(Theorem 1, identity of º)

      WP.r.R {s} R Ù WP.s.R {r} R

º(Weakest Precondition Axiom 2) 

      WP.r.R Í WP.s.R Ù WP.s.R Í WP.r.R

º(Set equality)

      WP.r.R = WP.s.R

End of Part 2 Proof

End of Proof

 

Corollary: WP.r.R = WP.s.R Þ P {r} R º P {s} R

(Prove LHS Þ RHS)

      WP.r.R = WP.s.R

º(Theorem 12)

                ("A|A {r} R º A {s} R:A)

(Instance)

      P {r} R º P {s} R

End of Proof

 

Theorem 13: ("B|WP.r.B = WP.s.B:B) º ("B|("A|A {r} B º A {s} B:A):B)

(Prove LHS º RHS)

("B|WP.r.B = WP.s.B:B) 

º(Theorem 12)

("B|("A|A {r} B º A {s} B:A):B)  

End of Proof

 

Theorem 14: (B Ç WP.r.R) {r} R

(proof uses ((True Þ P) º P)

(Theorem 1)

      WP.r.R {r} R

Þ(BÇP Í P, Theorem 6)

      (B Ç WP.r.R) {r} R

End of Proof       

 

Theorem 15: (P Ç WP.r.R) {s} R Ù (P Ç WP.s.R) {r} R Þ

            P Ç WP.r.R = P Ç WP.s.R

(Given (P Ç WP.r.R) {s} R,Prove LHS Í RHS)

(Given, Weakest Precondition Axiom 2)

      P Ç WP.r.R Í WP.s.R

Þ(Reflexive property of Í, monotonicity of Ç)

      P Ç P Ç WP.r.R Í P Ç WP.s.R

º(Idempotency of Ç)

      P Ç WP.r.R Í P Ç WP.s.R

End of Proof

 

Theorem 16: Æ {r} R

(Null set is subset of any set)

      ÆÍ WP.r.R

º(Weakest Precondition Axiom 2)

      Æ {r} R

End of Proof

 

Theorem 17: (P Í S Ù S {r} Q) Þ (P {r} R º P {r} (RÇQ))

(Given P Í S Ù S {r} Q, prove LHS º RHS)

P {r} R

º(Given, Corollary to Theorem 6, identity of Ù)

P {r} R Ù P {r} Q

º(Theorem 9)

P {r} (R Ç Q)

End of Proof

 

Corollary: (U {r} Q) Þ (P {r} R º P {r} (RÇQ))

(Given U {r} Q, prove LHS º RHS)

P {r} R

º(Given, P Í U, Theorem 17)

P {r} (R Ç Q)

End of Proof

 

Theorem 18: P = ƺ P {r} Æ

(Prove RHS º LHS)

      P {r} Æ

º(Weakest Precondition Axiom 2)

      P Í WP.r.Æ

º(Weakest Precondition Theorem 7)

      P ÍÆ

º(ÆÍ P, identity of Ù)

      P ÍÆÙÆÍ P

º(Set equality)

      P = Æ

End of Proof

 

Theorem 19: P {r} Q Ù P {r} ~Q º P = Æ

(Prove LHS º RHS)

P {r} Q Ù P {r} ~Q

º(Theorem 9)

P {r} (Q Ç ~Q)

º(QÇ~Q = Æ)

P {r} Æ

º(Theorem 18)

      P = Æ

End of Proof

 

 

 

 

References:

 

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

 

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