{ P:x/f } x := f { P }
{ 12 < 100 } d := 12 { d < 100 } { (3+r*z) >= 0 and m < (3+r*z) } k := 3 + r * z { k >= 0 and m < k }
exists x ( forall y ( y <= x ) )says there is MAXINT in your language.
{ P } S1 { Q }, { Q } S2 { R } ---------------------------------- { P } S1; S2 { R }Example:
{ 10 < 20 } a := 10 { a < 20 } { a < 20 } a := a + 5 { a < 25 }can be combined:
{ 10 < 20 } a := 10; a := a + 5 { a < 25 }
{ Q } S { R }, P ==> Q -------------------------- { P } S { R }Examples:
{ y + 5 > 10 } x := y + 5 { x > 10} can become { y > 5 } x := y + 5 { x > 10 } since y > 5 ==> y + 5 > 10 { y + 5 > 10 } x := y + 5 { x > 10 } can become { y + 5 > 15 } x := y + 5 { x > 10 } since y + 5 > 15 ==> y + 5 > 10
{ P } S { Q }, Q ==> R -------------------------- { P } S { R }Example:
{ x > 100 } x := x + 12 { x > 112 } can become { x > 100 } x := x + 12 { x > 0 } since x > 112 ==> x > 0
{ P and B } S { P } --------------------------------- { P } while B do S { P and ~B }Our 'invariant' is represented in the schematic as 'P'
The rule says that if P is invariant over one body execution,
then it is invariant over the entire life of the loop;
also, the loop body is traversed when the boolean is true, and
the boolean is false when the entire loop completes.
{ P and B } S { Q }, (P and ~B) ==> Q ---------------------------------------- { P } if B then S { Q }Examle of use in a proof.
{ P and B } S1 { Q }, { P and ~B } S2 { Q } ---------------------------------------------- { P } if B then S1 else S2 { Q }Examle of use in a proof.
forall i (1 <= i <= n ==> { P and C = Vi } Si { Q }) -------------------------------------------------- { P } case C of V1: S1; ... Vn: Sn; end { Q }
Here is a version in which the CASE has a default clause, to take effect if the variable C produces a value that is not represented in the CASE:
forall i ( 1 <= i <= n ==> { P and C = Vi } Si { Q } ) , { P and C!=V1 and C!= V2 and ... and C!=Vn } Sd { Q } ----------------------------------------------------- ----- { P } case C of V1: S1; ... Vn: Sn; default: Sd end { Q }
REPEAT S until B { Q and ~B } +--------------------------------+ | | V | -------------------->[ S ]--------------->< B >---------------> { P } { P } { Q } { Q and B }The inference rule we glean from this annotated flow diagram is as follows:
{ P } S { Q }, (Q and ~B) ==> P
------------------------------------- { P } repeat S until B { Q and B } |
Another way to get at a rule for REPEAT loops is to unfold the REPEAT into a loop body followed by a WHILE and then apply the WHILE rule and composition/consequence.