Programming Notes – Statement Sequence

 

 

Axiom 1: (r;s) = (r·s)

 

Axiom 2: T.(r;s) = WP.r.(T.s)

 

Theorem 1: WLP.(r;s).R = WLP.r.(WLP.s.R)

(Prove LHS = RHS)

      WLP.*(r;s).R

=(Axiom 1)

      WLP.(r·s).R

=(Weakest Liberal Precondition Theorem 7)

      ~dom.(r·s).~R

=(Composition Theorem 2)     

      ~dom.r.(dom.s.~R)

=(~~P = P)

      ~dom.r.(~~dom.s.~R)

=(Weakest Liberal Precondition Theorem 7)

      ~dom.r.(~WLP.s.R)

=(Weakest Liberal Precondition Theorem 7)

      WLP.r.(WLP.s.R)

End of Proof

 

Theorem 2: WP.(r;s).R = WP.r.(WP.s.R)

(prove RHS = LHS)

      WP.r.(WP.s.R)

=(Weakest Precondition Axiom 1)

      WP.r.(WLP.s.R Ç T.s)

=(Weakest Precondition Theorem 3)

      WP.r.(WLP.s.R) Ç WP.r.T.s

=(Weakest Precondition Axiom 1)

      WLP.r.(WLP.s.R)Ç T.rÇ WP.r.(T.s)

=(Weakest Precondition Theorem 8)

      WLP.r.(WLP.s.R) Ç WP.r.(T.s)

=(Axiom 2)

      WLP.r.(WLP.s.R) Ç T.(r;s)

=(Theorem 1)

      WLP.(r;s).R Ç T.(r;s)

=(Weakest Precondition Axiom 1)

      WP.(r;s).R

End of Proof     

 

Theorem 3: P {r} Q Ù S {s} R Ù Q Í S Þ P {r;s} R

(Prove LHS Þ RHS)

      P {r} Q Ù S {s} R Ù Q Í S

º(Weakest Precondition Axiom 2)

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

Þ(Weakest Precondition Theorem 2)

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

Þ(Weakest Precondition Theorem 2)

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

Þ(Transitivity of Í)

      P Í WP.r.(WP.s.R)

º(Theorem 2)

      P Í WP.(r;s).R)

º(Weakest Precondition Axiom 2)

      P {r;s} R

End of Proof

 

Theorem 4: P {r} Q Ù Q {s} R Þ P {r;s} R

(Theorem 3[S := Q])

P {r} Q Ù Q {s} R Ù Q Í Q Þ P {r;s} R

º(Reflexive Property of Í)

P {r} Q Ù Q {s} R Ù true Þ P {r;s} R

º(Identity of Ù)

P {r} Q Ù Q {s} R Þ P {r;s} R

End of Proof

 

Theorem 5: P {r;s} R º P {r} WP.s.R

(prove LHS º RHS)

      P {r;s} R  

º(Weakest Precondition Axiom 2)

      P Í WP.(r;s).R

º(Theorem 2)

      P Í WP.r.(WP.s.R)

º(Weakest Precondition Axiom 2)

      P {r} WP.s.R

End of Proof     

 

Corollary: P {r;s} R º P {r} WP.s.R Ù WP.s.R {s} R

(Theorem 5)

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

º(Programming Solutions Theorem 1, identity of Ù)

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

End of Proof

 

Theorem 6: P {r} Q Þ (P {r;s} R º P {r} (Q Ç WP.s.R))

(Given P {r} Q, Prove LHS º RHS)

P {r;s} R

º(Theorem 5)

      P {r} WP.s.R

º(given, identity of Ù)

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

º(Program Solution Theorem 9)

      P {r} (Q Ç WP.s.R)

End of Proof

 

Corollary: P {r} Q Þ (P {r;s} R º P {r} (Q Ç WP.s.R) Ù (Q Ç WP.s.R) {s} R)

(Prove LHS Þ RHS)

      P {r} Q

Þ(Theorem 6)

      P {r;s} R º P {r} (Q Ç WP.s.R

º(Program Solution Theorem 1, identity of Ù)

      P {r;s} R º P {r} (Q Ç WP.s.R) Ù (WP.s.R {s} R

Þ(PÇQ Í Q, Corollary to Program Solution Theorem 6)

      P {r;s} R º P {r} (Q Ç WP.s.R) Ù (Q Ç WP.s.R {s} R

End of Proof

 

Theorem 7: (P {r} WP.s.R º P {r} (QÇWP.s.R)) Þ

(P {r;s} R º P {r} (QÇWP.s.R) Ù (QÇWP.s.R) {s} R)

(Given P {r} WP.s.R º P {r} (QÇWP.s.R), prove LHS º RHS)

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

 

Case 1

(Given P {r} WP.s.R º P {r} (QÇWP.s.R), prove LHS Þ RHS)

      P {r;s} R

º(Theorem 5)

      P {r} WP.s.R

º(Given)

      P {r} (QÇWP.s.R)

º(Program Solution Theorem 1, Identity of Ù)

      P {r} (QÇWP.s.R) Ù WP.s.R {s} R

Þ(PÇQ Í Q, Corollary to Program Solution Theorem 6)

      P {r} (QÇWP.s.R) Ù (QÇWP.s.R) {s} R

End of Case 1 Proof

 

Case 2

(Given P {r} WP.s.R º P {r} (QÇWP.s.R), prove RHS Þ LHS)

      P {r} (QÇWP.s.R) Ù (QÇWP.s.R) {s} R

Þ(Theorem 4)

      P {r;s} R

End of Case 2 Proof

End of Proof

 

Theorem 8: (Associative Property) WP.((r;s);t).R = WP.(r;(s;t)).R

(Prove LHS = RHS)

      WP.((r;s);t).R

=(Theorem 2)

      WP.(r;s).(WP.t.R)

=(Theorem 2)

      WP.r.(WP.s.(WP.t.R))

=(Theorem 2)

      WP.r.(WP.(s;t).R))

=(Theorem 2)

      WP.(r;(s;t)).R

End of Proof

 

Theorem 9: P {r} WP.t.R º P {s} WP.t.R º P {r;t} R º P {s;t} R

(prove RHS º LHS)

      P {r;t} R º P {s;t} R

º(Theorem 5)

      P {r} WP.t.R º P {s;t} R

º(Theorem 5)

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

End of Proof

 

Theorem 10: WP.s.R = WP.t.R Þ P {r;s} R º P {r;t} R

(Given WP.s.R = WP.t.R, prove LHS º RHS)

      P {r;s} R

º(Theorem 5)

      P {r} WP.s.R

º(Given)

      P {r} WP.t.R

º(Theorem 5)

      P {s;t} R

End of Proof

 

Theorem 11: ("B|("A|A {r} B º A {a} B:A):B) Ù ("B|("A|A {s} B º A {b} B:A):B) Þ

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

(Given ("B|("A|A {r} B º A {a} B:A):B)

Ù ("B|("A|A {s} B º A {b} B:A):B),

      Prove RHS equivalence)

 

Part 1

(Given ("B|("A|A {r} B º A {a} B:A):B)

Ù ("B|("A|A {s} B º A {b} B:A):B)

Prove ("B WP.s.B º A a WP.b.B:B))

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

Ù ("B|("A|A {s} B º A {b} B:A):B)

Þ(aÙbÞb)

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

º(Program Solution Part 1 Theorem 12)

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

End of Part 1 Proof

 

Part 2

(Given ("B|("A|A {r} B º A {a} B:A):B)

Ù ("B|("A|A {s} B º A {b} B:A):B)

Prove ("B|("A|A {r;s} B º A {a;b} B:A):B)

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

Ù ("B|("A|A {s} B º A {b} B:A):B)

Þ(aÙbÞb)

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

Þ(Replace B with WP.s.B)

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

º(Given, Part 1)

      ("B|("A|A {r} WP.s.B º A {a} WP.b.B:A):B)

º(Corollary to Theorem 5)

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

End of Proof 

 

Theorem 12: P {r} Q Þ P {r;s} R º P {r} SR.r.R Ù SR.r.R {s} R

(Given P {r} Q, Prove LHS Þ RHS Ù RHS Þ LHS)

 

Part 1: Prove LHS Þ RHS

      P {r;s} R

º(Given, Strongest Result Theorem 6, Corollary to Theorem 6)

      P {r} SR.r.P Ç WP.s.R Ù SR.r.P Ç WP.s.R {s} R

Þ(weakening)

      P {r} SR.r.P Ç WP.s.R

Þ(Strongest Result Theorem 8)

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

º(idempotency of Ç)

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

º(Apply equality to second step)

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

End of Part 1 Proof

 

Part 2: Prove RHS Þ LHS

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

Þ(Theorem 4)

      P {r;s} R

End of Part 2 Proof

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

 

http://www.anaesthetist.com/mnm/javascript/index.htm Chapter 2 contains an excellent description of boolean operations in JavaScript.