Programming Notes – Flag Variable Theorems
Axiom 1: (flag is arbitrary) ØOccurs(flag, Q) (Q may be a precondition or an expected result)
Axiom 2: (scope of flag) WP.r.{x|flag=E} = {x|flag=E}ÇWP.r
Theorem 1: Given K is a constant of consistent type for Prog.x Ù
ØOccurs(Prog.x, P),
P {x := K} P Ç {State.s|: Prog.x = K}
(uses (true ÞP) º P)
(Given K is a constant of consistent type for Prog.x Ù
ØOccurs(Prog.x, P, prove the Hoare Triple is true)
(Given, Assignment Statement Theorem 9)
U {x := K} {State.s|: Prog.x = K}
Þ(Assignment Statement Theorem 3, Program Solution Theorem 7)
(P[x :=K] Ç dom.(x := K)ÇU) {x := K} (PÇ{State.s|: Prog.x = K})
º(Given, K is properly typed)
(P[x :=K] ÇUÇU) {x := K} (PÇ{State.s|: Prog.x = K})
º(Identity of Ç)
P[x :=K] {x := K} (PÇ{State.s|: Prog.x = K})
º(ØOccurs(x,P)
P {x := K} (PÇ{State.s|: Prog.x = K})
End of Proof
P {x := K} P Ç {State.s|: Prog.x = K}
(Given x is a flag variable, K is a constant of consistent type for Prog.x, P is a precondition or postcondition, prove that the Hoare triple is true)
(Given, Axiom 1)
K is a constant of consistent type for Prog.x ÙØOccurs(Prog.x, P)
Þ(Theorem 1)
P {x := K} (PÇ{State.s|: Prog.x = K})
End of Proof
Theorem 2: Given x is a flag variable, K is a constant of consistent type for Prog.x, P Ç Q, P are preconditions or postconditions,
P Ç Q (x := K) P Ç {State.s|: Prog.x = K}
(Given x is a flag variable, K is a constant of consistent type for Prog.x, P Ç Q, P are preconditions or postconditions, prove that the Hoare triple is true)
Use (True Þ P) º P
(Given, Corollary to Theorem 1)
P (x := K) P Ç {State.s|: Prog.x = K}
Þ(PÇQ Í P, Corollary to Program Solution Theorem 6)
PÇQ {x := K} P Ç {State.s|: Prog.x = K}
End of Proof
P {x := K} P
(Given x is a flag variable, K is a constant of consistent type for Prog.x, P is a precondition or postcondition, prove that the Hoare triple is true)
Use (True Þ P) º P
(Given, Theorem 1)
P {x := K} P Ç {State.s|: Prog.x = K}
Þ(PÇQ Í P, Corollary to Program Solution Theorem 5)
P {x := K} P
End of Proof
Theorem 4: Given x is a flag variable, K is a constant of consistent type for Prog.x, R is a precondition or postcondition,
P {x := K} (RÇ{State.s|:x=K}) º P {skip} R
(Show that the given items imply the equivalence)
x is a flag variable, K is a constant of consistent type for Prog.x, R is a precondition or postcondition.
º(axiom 1)
K is a constant of consistent type for Prog.x Ù Øoccurs(x,R).
P {x := K} (RÇ{State.s|:x=K}) º P {skip} R
End of Proof
Theorem 5: Given x is a flag variable, K is a constant of consistent type for Prog.x,
{State.s|:x¹K} {x := K} {State.s|:x=K}
(Use (True Þ P) º P)
(Given, Assignment Statement Theorem 9)
U {x := K} {State.s|: Prog.x = K}
Þ({State.s|:x = J} ÍU, Program Solution Theorem 6)
{State.s|:x ¹ K} {x := K} {State.s|: Prog.x = K}
End of Proof
Theorem 6: Given x and y are flag variables, J and K are constants of consistent type for Prog.x, Prog.y, respectively, and P is a precondition or postcondition,
P {x := J; y :=K} P Ç {State.s|:x=J}Ç{State.s|:y=K}
(Use (True Þ P) º P)
(Corollary to Theorem 1)
P {x := J} P Ç {State.s|:x = J}
º(Corollary to Theorem 1, identity of Ù)
P {x := J} P Ç {State.s|:x = J}
Ù
P Ç{State.s|:x = J} {y := K} P Ç {State.s|:x = J} Ç {State.s|:x = K}
Þ(Statement Sequence Theorem 4)
P {x := J; y := K} P Ç {State.s|:x = J} Ç {State.s|:x = K}
End of Proof
Theorem 7: Given x and y are flag variables, J and K are constants of consistent type for Prog.x, Prog.y, respectively, and P is a precondition or postcondition,
P Ç {State.s|:x¹J} {x := J; y :=K} P Ç {State.s|:x=J}Ç{State.s|:y=K}
(Use (True Þ P) º P)
(Given x and y are flag variables, J and K are constants of consistent type for Prob.x, Prog.y, respectively, and P is a precondition or postcondition)
(Given, Theorem 5)
{State.s|:x ¹ J} {x := J} {State.s|: Prog.x = J}
º(Theorem 1, identity of Ù)
{State.s|:x ¹ J} {x := J} {State.s|: Prog.x = J}
Ù
{State.s|:x = J} {y := K} {State.s|:x = J}Ç {State.s|: Prog.x = K}
º(Given, Theorem 3, identity of Ù)
{State.s|:x ¹ J} {x := J} {State.s|: Prog.x = J}
Ù
P {x := J} P
Ù
{State.s|:x = J} {y := K} {State.s|:x = J}Ç {State.s|: Prog.x = K}
Ù
P {y := K} P
P Ç {State.s|:x ¹ J} {x := J} P Ç {State.s|: Prog.x = J}
Ù
P Ç {State.s|:x = J} {y := K} P Ç {State.s|:x = J}Ç {State.s|: Prog.x = K}
Þ(Statement Sequence Theorem 4)
P Ç {State.s|:x ¹ J} {x := J;y := K} P Ç {State.s|:x = J}Ç {State.s|: Prog.x = K}
End of Proof
P {x := J;y :=K} (RÇ{State.s|:x=J} Ç{State.s|:y=K}) º P {skip} R
(Show that the given items imply the equivalence)
x is a flag variable, K is a constant of consistent type for Prog.x, R is a precondition or postcondition.
º(axiom 1)
K is a constant of consistent type for Prog.x Ù Øoccurs(x,R).
P {x := J;y :=K} (RÇ{State.s|:x=J} Ç{State.s|:y=K}) º P {skip} R
End of Proof
Theorem 9: Given x, y are flag variables, J, K are constants of consistent type for Prog.x and Prog.y, R is a precondition or postcondition,
P {x := J;y :=K} R º P {skip} R
(Show that the given items imply the equivalence)
x is a flag variable, K is a constant of consistent type for Prog.x, R is a precondition or postcondition.
º(axiom 1)
K is a constant of consistent type for Prog.x Ù Øoccurs(x,R).
P {x := J;y :=K} R º P {skip} R
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