Programming Notes – Strongest Result

 

Axiom 1: P {r} R Þ P {r) SR.r.P Ù SR.r.P Í R

 

Theorem 1: P {r} R º P {r} SR.r.P Ù SR.r.R Í R

(prove LHS Þ RHS Ù RHS Þ LHS)

 

Part 1 Prove RHS Þ LHS

P {r} SR.r.P Ù SR.r.R Í R

Þ(Corollary to Program Solution Part 1 Theorem 5)

P {r} R

End of Part 1 Proof    

 

Part 2 Prove LHS Þ RHS

P {r} R

Þ(Axiom 1)

P {r} SR.r.P Ù SR.r.R Í R

End of Part 2 Proof    

End of Proof     

 

Theorem 2: P {r} R Þ P Í T.r

(Prove LHS Þ RHS)

      P {r} R

º(Weakest Precondition Axiom 2)

      P Í WP.r.R

º(Weakest Precondition Axiom 1)

      P Í WLP.r.R Ç T.r

Þ(PÇQÍQ, transitivity of Í)

      P Í T.r

End of Proof

 

Theorem 3: P {r} R º P {r} ran.r.P

(Given P {r} R, Prove the Hoare Triple is true)

(Proof uses concept (True Þ P) º P)

(Reflexive property of Í)

      ran.r.P Í ran.r.P

º(Weakest Liberal Precondition Theorem 1)

      P Í WLP.r.(ran.r.P)

º(Theorem 2, identity of Ù)

      P Í WLP.r.(ran.r.P) Ù P Í T.r

º(Set Theorem)

      P Í WLP.r.(ran.r.P) Ç T.r

º(Weakest Precondition Axiom 1)

      P Í WP.r.(ran.r.P)

º(Weakest Precondition Axiom 2)

      P {r} ran.r.P

End of Proof

 

Theorem 4: P {r} R Þ ran.r.P Í R

(Prove LHS Þ RHS)

      P {r} R

º(Weakest Precondition Axiom 2)

      P Í WP.r.R

º(Weakest Precondition Axiom 1)

      P Í WLP.r.R Ç T.r

Þ(Weakening)

      P Í WLP.r.R

º(Weakest Liberal Precondition Theorem 1)

      ran.r.P Í R

End of Proof

 

Theorem 5: P {r} R Þ SR.r.P = ran.r.P

(Given P {r} R prove LHS = RHS in three parts)

 

Part 1: Prove Given Þ LHS Í RHS

 (given)

P {r} R

º(Theorem 1)

 P {r} SR.r.P Ù SR.r.R Í R

Þ(weakening)

 P {r} SR.r.P

Þ(Theorem 4)

      ran.r.P Í SR.r.P

End of Part 1 Proof

 

Part 2: Prove given Þ RHS Í LHS

(given)

P {r} R

º(Theorem 3)

      P {r} ran.r.P

º(Theorem 1)

P {r} SR.r.P Ù SR.r.R Í ran.r.R

Þ(weakening)

SR.r.R Í ran.r.R

End of Part 2 Proof

 

Part 3: Given P {r) R, prove RHS = LHS)

(Given, Part 1)

      ran.r.P Í SR.r.P

º(given, Part 2, identity of Ù)

ran.r.P Í SR.r.P ÙSR.r.R Í ran.r.R

º(set equality)

SR.r.R = ran.r.R

End of Part 3 Proof

End of Proof     

 

Theorem 6: P {r} Q Þ P {r} SR.r.P

(Prove LHS Þ RHS)

P {r} Q

Þ(Axiom 1)

P {r} SR.r.P Ù SR.r.R Í R

Þ(Weakening)

P {r} SR.r.P

End of Proof

 

Theorem 7: P {r} Q Þ SR.r.P Í Q

(Prove LHS Þ RHS)

P {r} Q

Þ(Axiom 1)

P {r} SR.r.P Ù SR.r.R Í Q

Þ(Weakening)

SR.r.R Í Q

End of Proof

 

 

Theorem 8: P {r} R Þ SR.r.P = SR.r.P Ç R

(prove LHS º RHS)

      P {r} R

º(Theorem 6, identity of Ù)

      P {r} R Ù P {r} SR.r.P

º(Program Solution Part 1 Theorem 9)

      P {r} R Ç SR.r.P

Þ(Theorem 7)

      SR.r.P Í R Ç SR.r.P

º(PÇQÍQ, identity of Ù)

      SR.r.P Í R Ç SR.r.P Ù R Ç SR.r.P Í SR.r.P

º(set equality

      SR.r.P = R Ç SR.r.P

End of Proof

 

Theorem 9: SR.r.Æ = Æ

(proof uses true Þ P º P)

(Program Solution Part 1 Theorem 16[R := Æ])

      Æ {r} Æ

Þ(Theorem 7)

      SR.r.ÆÍÆ

º(ÆÍSR.r.Æ, set equality)

      SR.r.Æ = Æ

End of Proof

 

Theorem 10: Given P Í Q, Q {r} R Þ SR.r.P Í SR.r.Q

(Given P Í Q, Prove LHS Þ RHS)

      Q {r} R

Þ(Theorem 6)

      Q {r} SR.r.Q

Þ(given, Program Solutions Part 1 Theorem 6)

      P {r} SR.r.Q

Þ(Theorem 7)

      SR.r.P Í SR.r.Q

End of Proof

 

Theorem 11: P {r} R Ù Q {r} S Þ SR.r.(PÇQ) Í (SR.r.P Ç SR.r.Q)

(Prove LHS Þ RHS)

      P {r} R Ù Q {r} S

Þ(Theorem 6)

      P {r} SR.r.P Ù Q {r} SR.r.Q

Þ(Program Solution Part 1 Theorem 7)

      (P Ç Q) {r} (SR.r.P Ç SR.r.Q)

Þ(Theorem 7)

      SR.r.(P Ç Q) Í (SR.r.P Ç SR.r.Q)

End of Proof

 

Theorem 12: P {r) R Ù Q {r} S Þ SR.r.(PÈQ) = (SR.r.P È SR.r.Q)

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

 

Part 1: prove Given Þ(LHS Í RHS)

(Given)

P {r} R Ù Q {r} S

Þ(Theorem 6)

      P {r} SR.r.P Ù Q {r} SR.r.Q

Þ(Program Solution Part 1 Theorem 8)

      (P È Q) {r} (SR.r.P È SR.r.Q)

Þ(Theorem 7)

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

End of Part 1 Proof

 

Part 2: prove Given Þ(LHS Í RHS)

(Given)

P {r} R Ù Q {r} S

Þ(Program Solution Part 1 Theorem 8)

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

Þ(Theorem 6)

      (P È Q) {r} SR.r.(P È Q)

Þ(P Í PÈQ, Theorem 9)

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

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

      SR.r.P Í SR.r.(PÈQ) Ù SR.r.Q Í SR.r.(PÈQ)

Þ(Set Theorem)

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

End of Part 2 Proof

 

Part 3: Consolidate results of Part 1 and Part 2

      (P È Q) {r} (R È S) ÞSR.r.(P È Q) Í (SR.r.P È SR.r.Q)

      Ù

      (P È Q) {r} (R È S) Þ(SR.r.P È SR.r.Q) Í SR.r.(PÈQ)

º((PÞQ Ù PÞR) º P Þ (QÙR))

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

Þ

(SR.r.(P È Q) Í (SR.r.P È SR.r.Q) ÙSR.r.P È SR.r.Q) Í SR.r.(PÈQ)

º(PÍQ Ù QÍP º P=Q)     

      (P È Q) {r} (R È S) Þ(SR.r.(P È Q) = (SR.r.P È SR.r.Q)

End of Part 3 Proof

End of Proof

 

Theorem 13: r is a function Þ SR.r.(dom.r.R) = ran.r.(dom.r.R)

(Given r is a function, prove the equality)

(Given, Program Solutions Part 1 Theorem 3)

      dom.r.R {r} R

º(Theorem 5)

      SR.r.(dom.r.R) = ran.r.(dom.r.R)

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