Programming Notes – if-statement Solution Part 1
Definition 1: IF[k,n] = (if (||i|k£i£n: (B[i]®r[i])) endif)
Definition 2: if endif = IF[false] = (if (||i|false: (B[i]®r[i])) endif)
Definition 3: I[k,n] = (||i|k£i£n: B[i]®r[i])
I[false] = (||i|false: B[i]®r[i])
Axiom 1: P {IF[k,n]} R º P {flag := true;G[k,n]} R
P {IF[false]} R º P {flag := true;G[false]} R
Theorem 1: P {if endif} Rº P {skip} R
(prove RHS Þ LHS Ù LHS Þ RHS)
Part 1: Prove RHS Þ LHS
P {skip} R
º(Flag Variable Axiom 1, Program Skip Theorem 7)
P {flag := true} (R Ç {s|:flag = true})
P {flag := true;skip} (R Ç {s|:flag = true})
º(Corollary to Program Sequence Part 1 Theorem 5)
P {flag := true} WP.skip.(R Ç {s|:flag = true}) Ù
WP.skip.(R Ç {s|:flag = true}) {skip} (R Ç {s|:flag = true})
º(Quantifying sequence axiom 1)
P {flag := true} WP.skip.(R Ç {s|:flag = true}) Ù
WP.skip.(R Ç {s|:flag = true})
{(;i|false:flag®(B[i]®(flag:=false;r[i])))}
(R Ç {s|:flag = true})
Þ(Program Sequence Part 1 Theorem 4)
P {flag := true;(;i|false:flag®(B[i]®(flag:=false;r[i])))}
(R Ç {s|:flag = true})
º(Axiom 1, Definition 1,2)
P {if endif} (R Ç {s|:flag = true})
Þ(PÇQ Þ P, Corollary to Program Solution Theorem 5)
P {if endif} R
End of Part 1 Proof
Part 2: Prove LHS Þ RHS
P {if endif} R
º(Guarded Command Sequence Definition 2, Axiom 1)
P {flag := true;G[false]} R
º(Corollary to Flag Variable Theorem 1, Corollary to Program Sequence Part 1 Theorem 6)
P {flag := true} (PÇ{s|:flag=true}ÇWP.G[false].R) Ù
PÇ{s|:flag=true}ÇWP.G[false].R) {G[false]} R
º(Guarded Command Sequence Definition 2, Quantifying Sequence Axiom 1)
P {flag := true} (PÇ{s|:flag=true}ÇWP.G[false].R) Ù
PÇ{s|:flag=true}ÇWP.G[false].R) {skip} R
Þ(Program Sequence Part 1 Theorem 4)
P {flag := true;skip} R
P {flag := true} R
Þ(Assignment Statement Theorem 9, Program Solution Theorem 7)
(PÇU){flag := true} (RÇ{s|:flag=true})
º(Identity of Ç)
P {flag := true} (RÇ{s|:flag=true})
P {skip} R
End of Part 2 Proof
End of Proof
Theorem 2: ("j|k£i£n:B[j] Í WP.r[j].R) Þ
("j|k£j£n:(B[j] Ç (Çi|k£i£ j-1:~B[i])) {IF[k,n]} R)
(Prove LHS Þ RHS)
("j|k£i£n:B[j] Í WP.r[j].R)
Þ(Corollary to Guarded Command Sequence Theorem 6)
("j|k£j£n: (B[j] Ç{s|flag=true} Ç(Çi|k£i£ j-1:~B[i])) {G[k,n]} R)
º(Corollary to Flag Variable Theorem 1, identity of Ù)
("j|k£j£n: (B[j] Ç(Çi|k£i£ j-1:~B[i]))
{flag := true}
(B[j] Ç{s|flag=true} Ç(Çi|k£i£ j-1:~B[i]))
Ù
(B[j] Ç{s|flag=true} Ç(Çi|k£i£ j-1:~B[i]))
{G[k,n]}
R)
Þ(Program Sequence Part 1 Theorem 4)
("j|k£j£n: (B[j] Ç(Çi|k£i£ j-1:~B[i])) {flag := true;G[k,n]} R)
º(Axiom 1)
("j|k£j£n: (B[j] Ç (Çi|k£i£ j-1:~B[i])) {IF[k,n]} R )
End of Proof
Theorem 3: ("j|k£j£n:B[j] Í WP.r[j].R) Þ
(Èj|k£j£n:B[j]) {IF[k,n]} R
(Given ("i|k£i£n:B[i] Í WP.r[i].R), prove that the Hoare Triple is true)
Þ(Given, Theorem 2)
("j|k£j£n: (B[j] Ç (Çi|k£i£ j-1:~B[i])) {IF[k,n]} R )
º(Program Solution Part 2 Theorem 4)
(Èj|k£j£n:(B[j] Ç (Çi|k£i£ j-1:~B[i]))) {IF[k,n]} R
º(Set Quantification Theorem 2)
(Èj|k£j£n:B[j]) {IF[k,n]} R
End of Proof
Theorem 4: (P Ç (Çi|k£i£n:~B[i])) {IF[k,n]} R º (P Ç (Çi|k£i£n:~B[i])) {skip} R
(prove RHS Þ LHS Ù LSS Þ RHS)
Part 1: Prove RHS Þ LHS
(P Ç (Çi|k£i£n:~B[i])) {skip} R
Þ(PÇQ Í Q, Program Solution Part 1 Theorem 6)
(P Ç (Çi|k£i£n:~B[i]) Ç {s|flag=True}) {skip} R
º(Guarded Command Sequence Part 1 Theorem 1)
(P Ç (Çi|k£i£n:~B[i]) Ç {s|flag=True}) {G[k,n]} R
º(Guarded Command Sequence Part 1 Theorem 8)
(P Ç (Çi|k£i£n:~B[i])) {flag:=True;G[k,n]} R
º(Axiom 1)
(P Ç (Çi|k£i£n:~B[i])) {IF[k,n]} R
End of Part 1 Proof
Part 1: Prove LHS Þ RHS
(P Ç (Çi|k£i£n:~B[i])) {IF[k,n]} R
º(Axiom 1)
(P Ç (Çi|k£i£n:~B[i])) {flag:=True;G[k,n]} R
º(Corollary to Flag Variable Theorem 1, Corollary to Program Sequence Part 1 Theorem 6)
(P Ç (Çi|k£i£n:~B[i]))
{flag := true}
(P Ç(Çi|k£i£n:~B[i])Ç{s|:flag=true}ÇWP.G[k,n].R)
Ù
(P Ç(Çi|k£i£n:~B[i])Ç{s|:flag=true}ÇWP.G[k,n].R)
{G[k,n]}
R
º(Guarded Command Sequence Part 1 Theorem 1)
(P Ç (Çi|k£i£n:~B[i]))
{flag := true}
(P Ç(Çi|k£i£n:~B[i])Ç{s|:flag=true}ÇWP.G[k,n].R)
Ù
(P Ç(Çi|k£i£n:~B[i])Ç{s|:flag=true}ÇWP.G[k,n].R)
{skip}
R
Þ(Program Sequence Part 1 Theorem 4)
(P Ç (Çi|k£i£n:~B[i])) {flag := true;skip} R
(P Ç (Çi|k£i£n:~B[i])) {flag := true} R
Þ(Assignment Statement Theorem 9, Program Solution Theorem 7)
(P Ç (Çi|k£i£n:~B[i]) ÇU) {flag := true} (R Ç{s|:flag=true})
º(Identity of Ç)
(P Ç (Çi|k£i£n:~B[i])) {flag := true} (R Ç{s|:flag=true})
(P Ç (Çi|k£i£n:~B[i])) {skip} R
End of Part 2 Proof
End of Proof
Theorem 5: (R Ç (Çi|k£i£n:~B[i])) {IF[k,n]} (R Ç (Çi|k£i£n:~B[i]))
(Prove that the Hoare Triple is true)
(Proof uses concept that (TrueÞ P) º P)
(R Ç (Çi|k£i£n:~B[i])) {skip} (R Ç (Çi|k£i£n:~B[i]))
º(Theorem 4)
(R Ç (Çi|k£i£n:~B[i]) Ç {s|flag=True}) {IF[k,n]} (R Ç (Çi|k£i£n:~B[i])
End of Proof
Corollary: (R Ç (Çi|k£i£n:~B[i])) {IF[k,n]} R
(Prove that the Hoare Triple is true)
(Proof uses concept that (TrueÞ P) º P)
(Theorem 5)
(R Ç (Çi|k£i£n:~B[i]))
{IF[k,n]}
(R Ç (Çi|k£i£n:~B[i])
Þ(PÇQ Í P, Program Solution Part 1 Theorem 5)
(R Ç (Çi|k£i£n:~B[i]))
{IF[k,n]}
R
End of Proof
Corollary: (R Ç (Çi|k£i£n:~B[i])) {IF[k,n]} (Çi|k£i£n:~B[i])
(Prove that the Hoare Triple is true)
(Proof uses concept that (TrueÞ P) º P)
(Theorem 5)
(R Ç (Çi|k£i£n:~B[i]))
{IF[k,n]}
(R Ç (Çi|k£i£n:~B[i])
Þ(PÇQ Í Q, Program Solution Part 1 Theorem 5)
(R Ç (Çi|k£i£n:~B[i]))
{IF[k,n]}
(Çi|k£i£n:~B[i])
End of Proof
Theorem 6: (Çi|k£i£n:~B[i]) Í R Þ
(Çi|k£i£n:~B[i]) {IF[k,n]} R
(Given (Çi|k£i£n:~B[i]) Í R, prove that the Hoare Triple is true)
(Corollary to Theorem 5)
(R Ç (Çi|k£i£n:~B[i])) {IF[k,n]} R
º(Given, P Í Q º PÇQ = P)
(Çi|k£i£n:~B[i]) {IF[k,n]} R
End of Proof
Theorem 7: ("j|k£j£n:B[j] Í WP.r[j].R) Ù (Çi|k£i£n:~B[i]) Í R Þ
U {IF[k,n]} R
(Prove LHS Þ RHS)
("j|k£j£n:B[j] Í WP.r[j].R) Ù (Çi|k£i£n:~B[i]) Í R
Þ(Theorem 3)
(Èj|k£j£n:B[j]) {IF[k,n]} R
º(Theorem 6, identity of Ù)
(Èj|k£j£n:B[j]) {IF[k,n]} R Ù (Çi|k£i£n:~B[i]) {IF[k,n]} R
º(Program Solution Part 1 Theorem 10)
((Èj|k£j£n:B[j]) È (Çi|k£i£n:~B[i])) {IF[k,n]} R
º(deMorgan)
((Èj|k£j£n:B[j]) È ~(Èi|k£i£n:B[i])) {IF[k,n]} R
º(PÈ~P = U)
U {IF[k,n]} R
End of Proof
Theorem 8: ("j|k£j£n:B[j] Í WP.r[j].R) Þ
(R Ç (Èj|k£j£n:B[j])) {IF[k,n]} R
(Given ("j|k£j£n:B[j] Í WP.r[j].R),Prove that the Hoare Triple is true)
(Given, Theorem 3)
(Èj|k£j£n:B[j]) {IF[k,n]} R
Þ(P Ç Q Í Q, Program Solution Part 1 theorem 6)
(R Ç (Èj|k£j£n:B[j])) {IF[k,n]} R
End of Proof
Theorem 9: ("j|k£j£n:B[j] Í WP.r[j].R) Þ
WP.IF[k,n].R = (Èj|k£j£n:B[j]) È R
(Given ("j|k£j£n:B[j] Í WP.r[j].R), prove set equality in four parts.
Part 1 proves LHS Í RHS, Parts 2, 3, 4 prove RHS Í LHS)
Part 1: (Èj|k£j£n:B[j]) È R Í WP.IF[k,n].R
(Theorem 3)
(Èj|k£j£n:B[j]) {IF[k,n]} R
º(Corollary to Theorem 4, identity of Ù)
(Èj|k£j£n:B[j]) {IF[k,n]} R
Ù
(R Ç (Çi|k£i£n:~B[i]))
{IF[k,n]}
R
º(Program Solution Part 1 Theorem 10)
(Èj|k£j£n:B[j]) È (R Ç (Çi|k£i£n:~B[i]))
{IF[k,n]}
R
º(distribute È over Ç)
(((Èj|k£j£n:B[j]) È R) Ç ((Èj|k£j£n:B[j]) È (Çi|k£i£n:~B[i]))
{IF[k,n]}
R
º(deMorgan, PÈ~P = U)
(((Èj|k£j£n:B[j]) È R) ÇU)
{IF[k,n]}
R
º(identity of Ç)
((Èj|k£j£n:B[j]) È R)
{IF[k,n]}
R
º(Weakest Precondition Axiom 2)
((Èj|k£j£n:B[j]) È R) Í WP.IF[k,n].R
End of Part 1 Proof
Part 2: Given {x} Í WP.IF[k,n].R, {x} Í (Çj|k£j£n:~B[j]) Þ {x} Í R
(Given {x} Í WP.IF[k,n].R, Prove LHS Þ RHS)
{x} Í (Çj|k£j£n:~B[j])
º(PÍQºPÇQ=P)
{x} = {x} Ç (Çi|k£i£n:~B[i])
º(Corollary to Theorem 5)
{x} {IF[k,n]} (Çi|k£i£n:~B[i])
º(Given, identity of Ù, Weakest Precondition Axiom 2)
{x} {IF[k,n]} (Çi|k£i£n:~B[i]) Ù {x} {IF[k,n]} R
º(Program Solutions Part 1 Theorem 9)
{x} {IF[k,n]} ((Çi|k£i£n:~B[i]) Ç R)
º({x} = {x} Ç (Çi|k£i£n:~B[i]), Theorem 4)
{x} {skip} ((Çi|k£i£n:~B[i]) Ç R)
Þ( PÍQºPÇQ=P, Program Solutions Part 1 Theorem 5)
{x} {skip} R
º(Weakest Precondition Axiom 2)
{x} Í WP.skip.R
{x} Í R
End of Part 2 Proof
Part 3: Given {x} Í WP.IF[k,n].R, {x} Í ((Èj|k£j£n:B[j]) È R)
(proof uses TrueÞPºP)
(Property of Universal set)
{x} ÍU
º(PÈ~P = U, DeMorgan)
{x} Í (Èj|k£j£n:B[j]) È (Çi|k£i£n:~B[i])
{x} Í (Èj|k£j£n:B[j]) Ú {x} Í (Çi|k£i£n:~B[i])
Þ(Part 2, monotonicity of Ú)
{x} Í (Èj|k£j£n:B[j]) Ú {x} Í R
{x} Í ((Èj|k£j£n:B[j]) È R)
End of Part 3 Proof
Part 4: WP.IF[k,n].R Í (Èj|k£j£n:B[j]) È R
(Reflexive property of Í)
WP.IF[k,n].R Í WP.IF[k,n].R
º(definition of Í)
("x|xÎWP.IF[k,n].R: xÎWP.IF[k,n].R)
("x|xÎWP.IF[k,n].R: {x}ÍWP.IF[k,n].R)
Þ(Part 4, monotonicity of ")
("x|xÎWP.IF[k,n].R: {x}Í((Èj|k£j£n:B[j]) È R))
("x|xÎWP.IF[k,n].R: xÎ((Èj|k£j£n:B[j]) È R))
º(definition of Í)
WP.IF[k,n].R Í ((Èj|k£j£n:B[j]) È R)
End of Part 4 Proof
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