Programming Notes - if-statements

Programming Notes – Guarded Command Sequences Part 1

Definition 1: G[k,n] = (;i|k£i£n:(flag®(B[i]®(flag:=false;r[i]))))

Definition 2: G[false] = (;i|false:(flag®(B[i]®(flag:=false;r[i]))))

Theorem 1:(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i])) {G[k,n]} R º

(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i])) {skip} R

Case n < k

(Given n < k, prove that the Hoare Triples are equivalent)

(P Ç {s|flag=true}Ç(Çi|k£i£n:~B[i]) {G[k,n]} R

º(Definition 1)

(P Ç {s|flag=true}Ç(Çi|k£i£n:~B[i])

{(i|k£i£n:flag®(B[i]®flag:=false;r[i]))}

R

º(Algebra)

(P Ç {s|flag=true}Ç(Çi|k£i£n:~B[i])

{(i|false:flag®(B[i]®flag:=false;r[i]))}

R

º(Quantifying sequences Axiom 1)

(P Ç {s|flag=true}Ç(Çi|k£i£n:~B[i])

{skip}

R

End of Proof Case n<k

Case n=k

(P Ç {s|flag=true}Ç(Çi|k£i£k:~B[i]) {G[k,k]} R

º(Definition 1)

(P Ç {s|flag=true}Ç(Çi|k£i£k:~B[i]))

{(i|k£i£k:flag®(B[i]®flag:=false;r[i]))}

R

º(Algebra, One point rule)

(P Ç {s|flag=true}Ç~B[k])

{(flag®(B[k]®flag:=false;r[k]))}

R

º(Guarded Command Theorem 11)

(P Ç {s|flag=true}Ç~B[k]) {skip} R

º(Algebra, One point rule)

(P Ç {s|flag=true}Ç(Çi|k£i£k:~B[i])) {skip} R

End of Proof Case n=k

Case n=m, n=m+1

(Given true for n=m, prove true for n=m+1)

(P Ç {s|flag=true}Ç(Çi|k£i£m+1:~B[i]) {G[k,m+1]} R

º(Definition 1, Split Range)

(P Ç {s|flag=true}Ç(Çi|k£i£m+1:~B[i]) {G[k,m];G[m+1,m+1]} R

º(split off term)

(P Ç {s|flag=true}Ç~B[m+1]Ç(Çi|k£i£m+1:~B[i]) {G[k,m];G[m+1,m+1]} R

º(Given, Case n=m is true [R := WP.G[m+1,m+1].R], Skip Statement Theorem 9)

(P Ç {s|flag=true}Ç~B[m+1]Ç(Çi|k£i£m:~B[i]) {G[m+1,m+1]} R

º(One Point Rule)

(P Ç {s|flag=true}Ç (Çi|m+1£i£m+1:~B[i])Ç(Çi|k£i£m:~B[i]) {G[m+1,m+1]} R

º(case n=k, above, where n=m+1)

(P Ç {s|flag=true}Ç (Çi|m+1£i£m+1:~B[i])Ç(Çi|k£i£m:~B[i]) {skip} R

º(split range)

(P Ç {s|flag=true}Ç(Çi|k£i£m+1:~B[i]) {skip} R

End of Proof Case m=m, n=m+1

End of Proof

Corollary: (P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))

{G[k,n]}

(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))

(Skip Statement Theorem 3)

(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))

{skip}

(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))

º(Theorem 1)

(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))

{G[k,n]}

(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))

End of Proof

Theorem 2: (P Ç {s|flag=false}) {G[k,n]} R º

(P Ç {s|flag=false}) {skip} R

Case n<k

(Given n<k, prove that LHS º RHS)

(P Ç {s|flag=false}) {G[k,n]} R

º(Definition 1)

(P Ç {s|flag=false})

{(i|k£i£n:flag®(B[i]®flag := false;r[i]))}

R

º(Given, Algebra)

(P Ç {s|flag=false})

{(i|false:flag®(B[i]®flag := false;r[i]))}

R

º(Quantifying sequences Axiom 1)

(P Ç {s|flag=false})

{skip}

R

End of Proof case n<k

Case n=k

(P Ç {s|flag=false}) {G[k,k]} R

º(Definition 1)

(P Ç {s|flag=false})

{(i|k£i£k:flag®(B[i]®flag:=false;r[i]))}

R

º(Algebra, One Point Rule)

(P Ç {s|flag=false})

{(flag®(B[k]®flag:=false;r[k]))}

R

º(Guarded Command Theorem 5)

(P Ç {s|flag=false}) {skip} R

End of Proof case n=k

Case n=m, n=m+1

(Given true for n=m, prove true for n=m+1)

(P Ç {s|flag=false}) {G[k,m+1]} R

º(Definition 1, Split Range)

(P Ç {s|flag=false}) {(G[k,m];G[m+1,m+1])} R

º(Given, Case n=m is true [R := WP.G[m+1,m+1].R], Skip Statement Theorem 9)

(P Ç {s|flag=false}) {G[m+1,m+1]} R

º(case, k=n, above, where n=m+1)

(P Ç {s|flag=false}) {skip} R

End of Proof Case m=m, n=m+1

End of Proof

Theorem 3: ({s|flag=false} Ç WP.G[k,n].R) = ({s|flag=false} Ç WP.skip.R)

(Prove LHS = RHS)

(Theorem 2[P := WP.G[k,n}.R])

({s|flag=false} Ç WP.G[k,n].R) {G[k,n]} R º

({s|flag=false} Ç WP.G[k,n].R) {skip} R

(Theorem 2[P := WP.skip.R], identity of Ù)

({s|flag=false} Ç WP.G[k,n].R) {G[k,n]} R º

({s|flag=false} Ç WP.G[k,n].R) {skip} R

Ù

({s|flag=false} Ç WP.skip.R) {G[k,n]} R º

({s|flag=false} Ç WP.skip.R) {skip} R

º(Program Solutions Theorem 14)

true º ({s|flag=false} Ç WP.G[k,n].R) {skip} R

Ù

{s|flag=false} Ç WP.skip.R) {G[k,n]} R º true

º(identity of º)

({s|flag=false} Ç WP.G[k,n].R) {skip} R

Ù

{s|flag=false} Ç WP.skip.R) {G[k,n]} R

Þ(Program Solution Theorem 15)

({s|flag=false} Ç WP.G[k,n].R) = {s|flag=false} Ç WP.skip.R)

End of Proof

Theorem 4: WP.(flag:=false; r).(RÇ{s|flag=false}) = WP.r.R

(Prove LHS = RHS)

WP.(flag:=false;r).(RÇ{s|flag=false})

=(Sequence Statement Theorem 1)

WP.(flag:=false).(WP.r.(RÇ{s|flag=false}))

=(Weakest Precondition Theorem 3)

WP.(flag:=false).(WP.r.RÇWP.r.{s|flag=false})

=(Axiom 2: scope of flag)

WP.(flag:=false).(WP.r.RÇ{s|flag=false}ÇWP.r)

=(Corollary to Weakest Precondition Theorem 2, PÍQ º PÇQ=P)

WP.(flag:=false).(WP.r.RÇ{s|flag=false})

=(Weakest Precondition Theorem 3)

WP.(flag:=false).(WP.r.R)

Ç

WP.(flag:=false).{s|flag=false})

=(Assignment Statement Theorem 10)

WP.(flag:=false).(WP.r.R)

Ç

U

=(identity of Ç)

WP.(flag:=false).(WP.r.R)

=(domain of flag assignment is Universal set, Assignment Statement Theorem 8)

(WP.r.R)[flag := false]

=(Flag Variable Axiom 1, rules of substitution)

(WP.r.R)

End of Proof

Theorem 5: B[j] Í WP.r[j].R Þ

(PÇB[j] Ç{s|flag=true}) {G[j,j]} (R Ç{s|flag=false})

(Prove LHS Þ RHS)

B[j] Í WP.r[j].R

Þ(AÇBÍB, transitivity of Ç)

PÇB[j] Í WP.r[j].R

Þ(AÇBÍB, transitivity of Ç)

(PÇB[j] Ç{s|flag=true}) Í WP.r[j].R

º(Theorem 4)

(PÇB[j] Ç{s|flag=true}) Í

WP.(flag:=false;r[j]).(RÇ{s|flag=false})

Þ(PÇAÇBÍAÇB, Guarded Command Theorem 9)

(PÇB[j] Ç{s|flag=true})

{flag®(B[j]®(flag:=false;r[j]))}

(RÇ{s|flag=false})

º(One point rule, definition 1)

(PÇB[j] Ç{s|flag=true}) {G[j,j]} (RÇ{s|flag=false})

End of Proof

Theorem 6: ("j|k£i£n:B[j] Í WP.r[j].R) Þ

("j|k£j£n:({s|flag=true} Ç B[j] Ç (Çi|k£i£ j-1:~B[i])) {G[k,n]} (RÇ{s|flag=false}))

(Prove LHS Þ RHS)

("j|k£j£n:B[j] Í WP.r[j].R)

Þ(Theorem 5, monotonicity of ")

("j|k£j£n: (B[j] Ç{s|flag=true}) {G[j,j]} (RÇ{s|flag=false}))

º(Right Identity)

("j|k£j£n: (B[j] Ç{s|flag=true}) {G[j,j];skip} (RÇ{s|flag=false})))

º(Program Sequence Part 1 Theorem 6)

("j|k£j£n: (B[j] Ç{s|flag=true})

{G[j,j]}

(R Ç{s|flag=false} Ç WP.skip.(RÇ{s|flag=false})))

º(Theorem 3)

("j|k£j£n: (B[j] Ç{s|flag=true})

{G[j,j]}

(R Ç{s|flag=false} Ç WP.(G[j+1,n]).(RÇ{s|flag=false})))

º(Program Sequence Part 1 Theorem 6)

("j|k£j£n: (B[j] Ç{s|flag=true}) {G[j,j];G[j+1,n]} (RÇ{s|flag=false}))

º(Definition 1, split range)

("j|k£j£n: (B[j] Ç{s|flag=true}) {G[j,n]} (RÇ{s|flag=false}))

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

("j|k£j£n: (B[j] Ç{s|flag=true} Ç(Çi|k£i£ j-1:~B[i]))

{G[j,n]}

(RÇ{s|flag=false}))

º(Theorem 1[R := WP.G[j,n].R, skip Statement Theorem 9)

("j|k£j£n: (B[j] Ç{s|flag=true} Ç(Çi|k£i£ j-1:~B[i]))

{G[k,j-1];G[j,n]}

(RÇ{s|flag=false}))

º(Definition 1, split range)

("j|k£j£n: (B[j] Ç{s|flag=true} Ç(Çi|k£i£ j-1:~B[i])) {G[k,n]} (RÇ{s|flag=false}))

End of Proof

Corollary: ("j|k£i£n:B[j] Í WP.r[j].R) Þ

("j|k£j£n:({s|flag=true} Ç B[j] Ç (Çi|k£i£ j-1:~B[i])) {G[k,n]} R

(Proof uses (True Þ P) º P)

(Theorem 6)

("j|k£i£n:B[j] Í WP.r[j].R) Þ

("j|k£j£n:({s|flag=true} Ç B[j] Ç (Çi|k£i£ j-1:~B[i])) {G[k,n]} (RÇ{s|flag=false}))

Þ(PÇQÍP, Program Solution Theorem 5, Transitivity of Þ)

("j|k£j£n: (B[j] Ç{s|flag=true}) {G[j,j]} R))

End of Proof

Theorem 7: ("j|k£j£n:B[j] Í WP.r[j].R) Þ

({s|flag=true} Ç (Èj|k£j£n:B[j]) {G[k,n]} (RÇ{s|flag=false}

(Given k£n Ù ("i|k£i£n:B[i] Í WP.r[i].R), prove that the Hoare Triple is true)

Þ(Theorem 6)

("j|k£j£n:({s|flag=true} Ç B[j] Ç (Çi|k£i£ j-1:~B[i])) {G[k,n]} (RÇ{s|flag=false}))

º(Program Solution Part 2 Theorem 4)

(Èj|k£j£n: ({s|flag=true} Ç B[j] Ç (Çi|k£i£ j-1:~B[i])) {G[k,n]} (RÇ{s|flag=false}

º(distribute Ç over È)

({s|flag=true} Ç (Èj|k£j£n: (B[j] Ç (Çi|k£i£ j-1:~B[i]))) {G[k,n]} (RÇ{s|flag=false})

º(Set Quantification Theorem 2)

({s|flag=true} Ç (Èj|k£j£n: B[j])) {G[k,n]} (RÇ{s|flag=false})

End of Proof

Theorem 8: (P Ç {s|flag=true:s}) {G[k,n]} R º P {flag := true;G[k,n]} R

(Prove by showing RHS Þ LHS Ù LHS Þ RHS)

Part 1: Prove LHS Þ RHS

P {flag := true;G[k,n]} R

º(Flag Variable Theorem 3, Corollary to Statement Sequence Theorem 6)

P {flag := true} (PÇWP.(G[k,n]).R)

Ù

(PÇWP.(G[k,n]).R) {G[k,n]} R

º(Flag Variable Theorem 1, Identity of Ù)

P {flag := true} (PÇ{s|flag=true:s})

Ù

P {flag := true} (PÇWP.(G[k,n]).R)

Ù

(PÇWP.(G[k,n]).R) {G[k,n]} R

º(Program Solutions Theorem 9, Ç is idempotent)

P {flag := true} (PÇ{s|flag=true:s}ÇWP.(G[k,n]).R)

Ù

(PÇWP.(G[k,n]).R) {G[k,n]} R

º(Flag Variable Theorem 4)

P {skip} (PÇWP.(G[k,n]).R)

Ù

(PÇWP.(G[k,n]).R) {G[k,n]} R

º(skip Statement Theorem 3, Corollary to Statement Sequence Theorem 6

P {skip;G[k,n]} R

º(Left identity)

P {G[k,n]} R

Þ(PÇQÍP, Program Solutions Part 1 Theorem 6)

(P Ç {s|flag=true:s}) {G[k,n]} R

End of Part 1 Proof

Part 2: Prove RHS Þ LHS

(P Ç {s|flag=true:s}) {G[k,n]} R

º(Corollary to Flag Variable Theorem 1, identity of Ù)

P {flag := true} (PÇ{s|: flag=true:s})

Ù

(P Ç {s|flag=true:s}) {G[k,n]} R

Þ(Statement Sequences Theorem 4)

P {flag := true;G[k,n]} R

End of Part 2 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