Programming Notes – Weakest Liberal Pecondition
Axiom 1: x Î T.rºØ("y|:Ø(x r y))
Axiom 2: ("x,y|xÎP:x r y Þ yÎR) º PÍWLP.r.R
Theorem 1: P Í WLP.r.R º ran.r.P Í R
(Axiom 2)
("x,y|xÎP:xry Þ yÎR)ºPÍWLP.r.R
º(Corollary to Relations Part 3 Theorem 5, identity of Ù)
("x,y|xÎP:xry Þ yÎR)ºPÍWLP.r.R
Ù
("x,y|xÎP: xry Þ y Î R)º ran.r.P Í R
º(transitivity of º)
P Í WLP.r.R º ran.r.P Í R
End of Proof
Theorem 2: T.r = dom.r
(prove LHS = RHS using set membership)
(reflexive property of =)
T.r = T.r
º(set equality)
("x|:x Î T.rº x Î T.r)
º(Axiom 1)
("x|:x Î T.rºØ("y|:Ø(xry)))
º(deMorgan)
("x|:x Î T.rº ($y|:xry))
º(one point rule)
("x|:x Î T.rº ($a|($y|:ary):x=a))
º(set membership)
("x|:x Î T.rº xÎ{a|($y|:ary):a})
º(definition of dom.r)
("x|:x Î T.rº x Î dom.r)
º(defintion of set =)
T.r = dom.r
End of Proof
Theorem 3: P Í Q Þ WLP.r.P Í WLP.r.Q
(Given P Í Q, prove LHS Í RHS)
(Reflexive property of Í)
WLP.r.P Í WLP.r.P
º(Theorem 1)
ran.r.(WLP.r.P) Í P
º(given, identity of Ù)
ran.r.(WLP.r.P) Í P Ù P Í Q
Þ(Transitivity of Í)
ran.r.(WLP.r.P) Í Q
º(Theorem 1)
WLP.r.P Í WLP.r.Q
End of Proof
Theorem 4: WLP.r.P Ç WLP.r.Q = WLP.r.(PÇQ)
(prove LHS Í RHS Ù RHS Í LHS)
(Part 1 prove LHS Í RHS)
(Reflexive property of Í)
WLP.r.P Í WLP.r.P Ù WLP.r.Q Í WLP.r.Q
º(Theorem 1)
(ran.r.(WLP.r.P) Í P) Ù
(ran.r.(WLP.r.Q) Í Q)
Þ(monotonicity of Ç)
(ran.r.(WLP.r.P) Ç ran.r.(WLP.r.Q)) Í (P Ç Q)
Þ(relations part 2 Theorem 9, transitivity of Í)
ran.r.(WLP.r.P Ç WLP.r.Q) Í (P Ç Q)
º(Theorem 1)
(WLP.r.P Ç WLP.r.Q) Í WLP.r.(P Ç Q)
End of Part 1 Proof
(Part 2 prove RHS Í LHS)
(prove using (True Þ P) Þ P
(Reflexive property of Í)
(WLP.r.(PÇQ) Í (WLP.r.(PÇQ)
º(Theorem 1)
ran.r.(WLP.r.(PÇQ)) Í (PÇQ)
º(Ù is idempotent)
ran.r.(WLP.r.(PÇQ)) Í (PÇQ) Ù ran.r.(WLP.r.(PÇQ)) Í (PÇQ)
Þ(transitivity of Í, PÇQ Í P)
ran.r.(WLP.r.(PÇQ)) Í P Ù ran.r.(WLP.r.(PÇQ)) Í Q
º(Theorem 1)
WLP.r.(PÇQ) Í WLP.r.P Ù WLP.r.(PÇQ) Í WLP.r.Q
Þ((PÍQ) Ù (PÍR) Þ (PÍ QÇR))
WLP.r.(PÇQ) Í WLP.r.P Ç WLP.r.Q
End of Part 2 Proof
End of Proof
Theorem 5: WLP.r.P È WLP.r.Q Í WLP.r.(PÈQ)
(prove using (True Þ P) Þ P)
(Reflexive property of Í)
WLP.r.P Í WLP.r.P Ù WLP.r.Q Í WLP.r.Q
º(Theorem 1)
(ran.r.(WLP.r.P) Í P) Ù
(ran.r.(WLP.r.Q) Í Q)
Þ(monotonicity of È)
ran.r.(WLP.r.P) È ran.r.(WLP.r.Q) Í PÈQ
ran.r.(WLP.r.P È WLP.r.Q) Í PÈQ
º(Theorem 1)
(WLP.r.P È WLP.r.Q) Í WLP.r.(PÈQ)
End of Proof
Theorem 6: ("X|:(~WLP.r.X = WLP.r.~X)) Þ (WLP.r.(RÈQ) = WLP.r.R È WLP.r.Q)
(Given ~WLP.r.R = WLP.r.~R, prove LHS = RHS)
WLP.r.(RÈQ)
=(DeMorgan)
WLP.r.~(~RÇ~Q)
=(given)
~WLP.r.(~RÇ~Q)
=(Theorem 4)
~(WLP.r.~R Ç WLP.r.~Q)
=(given)
~(~WLP.r.R Ç~WLP.r.Q)
=(DeMorgan)
WLP.r.R È WLP.r.Q
End of Proof
Theorem 7: WLP.r.R = ~dom.r.(~R)
(Prove by showing LHS = RHS)
(Set equality is reflexive)
WLP.r.R = WLP.r.R
º(Definition of set =)
("x|:x Î WLP.r.R º x Î WLP.r.R)
("x|:x Î WLP.r.R º {x} Í WLP.r.R)
º(Theorem 1)
("x|:x Î WLP.r.R º ran.r.{x} Í R)
º(definition of Í)
("x|:x Î WLP.r.R º ("y| y Î ran.r.{x}: y Î R))
º(Relations Part 2 Theorem 13)
("x|:x Î WLP.r.R º ("y| x r y: y Î R))
º(Trading)
("x|:x Î WLP.r.R º ("y|: Ø(x r y) Ú y Î R))
º(deMorgan
("x|:x Î WLP.r.R ºØ($y|: (x r y) ÙØ(y Î R)))
º(One Point Rule)
("x|:x Î WLP.r.R ºØ($a($y|: (a r y) ÙØ(y Î R)):a=x))
º(definition of Î)
("x|:x Î WLP.r.R ºØ(x Î {a($y|: (a r y) ÙØ(y Î R)):a}))
º(definition of set complement)
("x|:x Î WLP.r.R º x Î ~{a($y|: (a r y) Ù y Î ~R):a})
º(definition of dom.r.(~R))
("x|:x Î WLP.r.R º x Î ~dom.r.(~R))
º(Definition of set =)
WLP.r.R = ~dom.r.(~R)
End of Proof
Theorem 8: ("x,y|: x Î WLP.r.R Ù x r y Þ y Î R)
(Þ is reflexive, Ù is symmetric)
("x,y|: xÎWLP.r.R Ù xry Þ xry Ù xÎWLP.r.R)
("x,y|: xÎWLP.r.R Ù xry Þ xry Ù {x} Í WLP.r.R)
º(Theorem 1)
("x,y|: xÎWLP.r.R Ù xry Þ xry Ù ran.r.{x} Í R)
º(Relations Part 2 Theorem 13)
("x,y|: xÎWLP.r.R Ù xry Þ yÎran.r.{x} Ù ran.r.{x} Í R)
("x,y|: xÎWLP.r.R Ù xry Þ {y}Íran.r.{x} Ù ran.r.{x} Í R)
Þ(transitive property of Í)
("x,y|: xÎWLP.r.R Ù xry Þ {y} Í R)
("x,y|: xÎWLP.r.R Ù xry Þ y Î R)
End of Proof
Theorem 9: WLP.r.Æ Í ~T.r
(Theorem 8[R := Æ])
("x,y|: xÎWLP.r.ÆÙ xry Þ y ÎÆ)
º(nesting)
("x|:("y|:xÎWLP.r.ÆÙ xry Þ y ÎÆ))
º(Shunting)
("x|:("y|:xÎWLP.r.ÆÞ(xry Þ y ÎÆ)))
º(pÞqºØpÚq, distribute Ú over ")
("x|:xÎWLP.r.ÆÞ("y|:xry Þ y ÎÆ))
º(pÞq ºØqÞØp)
("x|:xÎWLP.r.ÆÞ("y|:yÏÆÞØ(xry)))
º(Null sets have no members, left identity of Þ)
("x|:xÎWLP.r.ÆÞ("y|:Ø(xry)))
º(a ºØØa)
("x|:xÎWLP.r.ÆÞØØ("y|:Ø(xry)))
º(Axiom 1)
("x|:xÎWLP.r.ÆÞ xÏT.r)
º(Complementary sets)
("x|:xÎWLP.r.ÆÞ xÎ~T.r)
º(Definition of subset)
WLP.r.ÆÍ ~T.r
End of Proof
Theorem 10: r is a function Þ dom.r.R Í WLP.r.R
(given, Relations Part 4 Theorem 5)
ran.r.(dom.r.R) Í R
º(Theorem 1)
dom.r.R Í WLP.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