Programming Notes – Program if-statements – Guarded Commands
Axiom 1: (Guarded Command Solution) PÍ B Þ P {B®r} R º P {r} R
Axiom 2: (Guarded Command Solution) P Í ~B Þ P {B®r} R º P {skip} R
Definition 1: GC[k,n] = (;i|k£i£n:B[i]®r[i])
Theorem 1: B Í WP.r.R Ù P Í B Þ P {B®r} R
(Prove LHS Þ RHS)
B Í WP.r.R Ù P Í B
Þ(Axiom 1, identity of Ù)
B Í WP.r.R Ù P Í B Ù (P {B®r} R º P r R)
º(Weakest Precondition Axiom 2)
B {r} R Ù P Í B Ù (P {B®r} R º P {r} R)
Þ(Corollary to Program Solutions Theorem 6)
P {r} R Ù (P {B®r} R º P {r} R)
º(A Ù (AºB) º A Ù B)
P {r} R Ù P {B®r} R
Þ(Weakening)
P {B®r} R
End of Proof
Theorem 2: B Í WP.r.R Þ B {B®r} R
(Theorem 1)
B Í WP.r.R Ù B Í B Þ B {B®r} R
º(Reflexive property of Í)
B Í WP.r.R Ù true Þ B {B®r} R
º(Identity of Ù)
B Í WP.r.R Þ B {B®r} R
End of Proof
Theorem 3: B Í WP.r.R Þ B Í WP.(B®r).R
(Theorem 2)
B Í WP.r.R Þ B {B®r} R
º(Weakest Precondition Axiom 2)
B Í WP.r.R Þ B Í WP.(B®r).R
End of Proof
Theorem 4: (P Ç B) {B®r} R º (P Ç B) {r} R
(proof uses (True Þ R) º R)
(Set Theorem)
P Ç B Í B
Þ(Axiom 1)
(P Ç B) {B®r} R º (P Ç B) {r} R
End of Proof
Theorem 5: (P Ç ~B) {B®r} R º (P Ç ~B) {skip} R
(proof uses (True Þ R) º R)
(Set Theorem)
P Ç ~B Í ~B
Þ(Axiom 2)
(P Ç ~B) {B®r} R º (P Ç ~B) {skip} R
End of Proof
Theorem 6: ~B {B®r} R º ~B {skip} R
(Proof uses (True Þ P) º P)
(Theorem 5, Property of Ç)
(~B Ç ~B) {B®r} R º (~B Ç ~B) {skip} R
º(Reflexive property of Ç)
~B {B®r} R º ~B {skip} R
End of Proof
Theorem 7: RÇ~B {B®r} RÇ~B
RÇ~B {skip} RÇ~B
º(Theorem 5)
RÇ~B {B®r} RÇ~B
End of Proof
Corollary: RÇ~B {B®r} ~B
(proof uses (True Þ R) º R)
(Theorem 7)
RÇ~B {B®r} RÇ~B
Þ(PÇQÍQ, Program Solution Part 1 Theorem 5)
RÇ~B {B®r} ~B
End of Proof
Corollary: RÇ~B {B®r} R
(proof uses (True Þ R) º R)
(Theorem 7)
RÇ~B {B®r} RÇ~B
Þ(PÇQÍP, Program Solution Part 1 Theorem 5)
RÇ~B {B®r} R
End of Proof
Theorem 8: B Í WP.r.R Þ WP.(B®r).R = BÈR
(Given B Í WP.r.R, prove set equality in four parts.
Part 1 proves LHS Í RHS, Parts 2, 3, 4 prove RHS Í LHS)
Part 1: B È R Í WP.(B®r).R
(Given, Theorem 2)
B {B®r} R
º(Corollary to Theorem 7, identity of Ù)
B {B®r} R Ù (R Ç ~B) {B®r} R
º(Program Solution Part 1 Theorem 10)
B È (R Ç ~B) {B®r} R
º(distribute È over Ç)
((B È ~B) Ç (BÈR)) {B®r} R
º(deMorgan, PÈ~P = U)
(UÇ (BÈR)) {B®r} R
º(identity of Ç)
(BÈR) {B®r} R
º(Weakest Precondition Axiom 2)
B È R Í WP.(B®r).R
End of Part 1 Proof
Part 2: Given {x} Í WP.(B®r).R, {x} Í ~B Þ {x} Í R
(Given {x} Í WP.(B®r).R, Prove LHS Þ RHS)
{x} Í ~B
º(PÍQºPÇQ=P)
{x} = {x} Ç ~B
º(Corollary to Theorem 7)
{x} {B®r} ~B
º(Given, identity of Ù, Weakest Precondition Axiom 2)
{x} {B®r} ~B Ù {x} {B®r} R
º(Program Solutions Part 1 Theorem 9)
{x} {B®r} (~B Ç R)
º({x} = {x} Ç (Çi|k£i£n:~B[i]), Theorem 5)
{x} {skip} (~B Ç 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.(B®r).R, {x} Í (B È R)
(proof uses TrueÞPºP)
(Property of Universal set)
{x} ÍU
º(PÈ~P = U, DeMorgan)
{x} Í (B È ~B)
{x} Í B Ú {x} Í ~B
Þ(Part 2, monotonicity of Ú)
{x} Í B Ú {x} Í R
{x} Í (B È R)
End of Part 3 Proof
Part 4: WP.(B®r).R Í (B È R)
(Reflexive property of Í)
WP.(B®r).R Í WP.(B®r).R
º(definition of Í)
("x|xÎWP.(B®r).R: xÎWP.(B®r).R)
("x|xÎWP.(B®r).R: {x}ÍWP.(B®r).R)
Þ(Part 4, monotonicity of ")
("x|xÎWP.(B®r).R: {x}Í(B È R))
("x|xÎWP.(B®r.R: xÎ(B È R))
º(definition of Í)
WP.(B®r).R Í (B È R))
End of Part 4 Proof
End of Proof
Theorem 9: B Í WP.r.R Ù P Í A Ç B Þ P {A®(B®r)} R
(Prove LHS Þ RHS)
B Í WP.r.R Ù P Í A Ç B
Þ(P Í AÇB Þ P Í B, Theorem 1)
P {B®r} R Ù P Í A Ç B
Þ(P Í AÇB Þ P Í A, Axiom 1)
P {B®r} R Ù (P {A®(B®r)} R º P {B®r} R)
º(A Ù (AºB) º A Ù B)
P {B®r} R Ù P (A®(B®r)) R
Þ(Weakening)
P (A®(B®r)) R
End of Proof
Theorem 10: P Í A Ç ~B Þ P {A®(B®r)} R º P {skip} R
(Given P Í A Ç ~B, prove LHS º RHS)
P {A®(B®r)} R
º(Given, P Í AÇ~B Þ P Í A, Axiom 1)
P {B®r} R
º(Given, P Í AÇ~B Þ P Í ~B, Axiom 2)
P {skip} R
End of Proof
Theorem 11: (P Ç A Ç ~B) {A®(B®r)} R º (P Ç A Ç ~B) {skip} R
(Prove using (True Þ P) º P)
(Set Theorem)
P Ç A Ç ~B Í A Ç ~B
Þ(Theorem 10)
(P Ç A Ç ~B) {A®(B®r)} R º (P Ç A Ç ~B) {skip} R
End of Proof
Theorem 12: (P Ç (Ç|k£i£n:~B[i]) {GC[k,n]} R º
(P Ç (Ç|k£i£n:~B[i]) {skip} R
Case n=k
(P Ç (Ç|k£i£k:~B[i]) {GC[k,k]} R
º(Definition 1)
(P Ç (Ç|k£i£k:~B[i]) {(i|k£i£k:(B[i]®r[i])} R
º(Algebra, One point rule)
(P Ç ~B[k]) {B[k]®r[k]} R
º(Theorem 5)
(P Ç ~B[k]) {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 Ç (Ç|k£i£m+1:~B[i]) {GC[k,m+1]} R
º(Definition 1, Split Range)
(P Ç (Ç|k£i£m+1:~B[i]) {GC[k,m];GC[m+1,m+1]} R
º(Definition 1, Split Range)
(P Ç ~B[m+1]Ç(Ç|k£i£m:~B[i]) {GC[k,m];GC[m+1,m+1]} R
(P Ç ~B[m+1]Ç(Ç|k£i£m:~B[i]) {GC[k,m]} WP.GC[m+1,m+1].R
º(Given true for case n=m)
(P Ç ~B[m+1]Ç(Ç|k£i£m:~B[i]) {skip} WP.GC[m+1,m+1].R
(P Ç ~B[m+1]Ç(Ç|k£i£m:~B[i]) {skip;GC[m+1,m+1]} R
(P Ç ~B[m+1]Ç(Ç|k£i£m:~B[i]) {GC[m+1,m+1]} R
º(case n=k[k := m+1])
(P Ç ~B[m+1]Ç(Ç|k£i£m:~B[i]) {skip} R
º(Split Range)
(P Ç (Ç|k£i£m+1:~B[i]) {skip} R
End of Proof Case m=m, n=m+1
End of Proof
Theorem 13: P {true®r} R º P {r} R
(Prove LHS º RHS)
P {true®r} R
º(P = PÇU)
(PÇU) {true®r} R
(PÇ{s|true:s}) {true®r} R
º(Theorem 4)
(PÇ{s|true:s}) {r} R
(PÇU) {r} R
º(P = PÇU)
P {r} R
End of Proof
Theorem 14: P {false®r} R º P {skip} R
(Prove LHS º RHS)
P {false®r} R
º(P = PÇU)
(PÇU) {false®r} R
º(U = ~Æ)
(PÇ~Æ) {false®r} R
(PÇ ~{s|false:s}) {false®r} R
º(Theorem 5)
(PÇ ~{s|false:s}) {skip} R
(PÇ ~Æ) {skip} R
º(U = ~Æ)
(PÇU) {skip} R
º(P = PÇU)
P {skip} 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