Rules of Hoare logic.

For the language of while loops, there are six rules of Hoare
logic.


    P {skip} P                                            [skip]


    -----------------                               [assignment]
    P[E/x] {x := E} P


      P0 {S1} P1
      P1 {S2} P2
    --------------                                 [composition]
    P0 {S1; S2} P2


           pre and B {S1} post
       pre and not B {S2} post
   -------------------------------                 [conditional]
   pre {if B then S1 else S2} post


         inv and B {S} inv
   --------------------------------                      [while]
   inv {while B do S} inv and not B


    P implies Q
    T implies U
    Q {S} T
    -----------                                    [subsumption]
    P {S} U

****************************************************************

To show that a while loop is correct:

1.  Formulate the loop invariant.

2.  Prove that the precondition
    implies the loop invariant.

3.  Prove that the loop invariant
    and the test together imply
    that the body of the loop
    preserves the loop invariant.

4.  Prove that the loop invariant
    and the negation of the test
    together imply the postcondition.

5.  Prove that the loop terminates.

Steps 1 through 4 constitute partial correctness.
Steps 2 and 4 correspond to the [subsumption] rule of Hoare logic.
Step 3 corresponds to the [while] rule of Hoare logic.

****************************************************************

Example using Hoare logic.

IntSet intersection ( IntSet s1, IntSet s2 ) {
    IntSet x1 = s1;
    IntSet s3 = emptySet();
    int n;

    //  Loop invariant:
    //  s1 \intersect s2  =  s3 \union (x1 \intersect s2)

    while (! isEmpty (x1)) {
        n = choose (x1);
        x1 = remove (n, x1);
        if (isElementOf (n, s2))
            s3 = adjoin (n, s3);
    }

    return s3;
}

****************************************************************

Abbreviations for statements.

Let C1 be

    n = choose (x1);

Let C2 be

    x1 = remove (n, x1);

Let C3 be

    s3 = adjoin (n, s3);

Let C4 be

    if (isElementOf (n, s2)) C3

Let C5 be

    while (! isEmpty (x1)) { C1; C2; C4 }

****************************************************************

Abbreviations for assertions.

Let PRE be  R(x1) = R(s1)  and  R(s3) = { }

Let POST be R(s1) \intersect R(s2) = s3

Let INV be  R(s1) \intersect R(s2)
                = R(s3) \union (R(x1) \intersect R(s2))

Let A be    R(x1) is nonempty

Let B be    n \in R(x1)

Let C be    R(s1) \intersect R(s2)
                = R(s3) \union (({ n } \union R(x1))
                                \intersect R(s2))

****************************************************************

Proof of PRE { C5 } POST

Partial correctness assertions 1b, 2b, 3b, and 4b follow from
the subsumption rule applied to the preceding assertion.

 1a. INV and A and choose(x1) \in R(x1) { C1 } INV and A and B

 1b. INV and A { C1 } INV and A and B

 2a. R(s1) \intersect R(s2)
         = R(s3) \union (({ n } \union R(remove (n, x1)))
                         \intersect R(s2))
     { C2 }
     C

 2b. INV and A and B { C2 } C

 3a. R(s1) \intersect R(s2)
         = R({ n } \union s3) \union (R(x1) \intersect R(s2))
     { C3 }
     INV

 3b. C and n \in s2 { C3 } INV

 4a. INV { skip } INV

 4b. C and n \not\in s2 { skip } INV

 5.  C { C4 } INV

 6.  INV and A { C1; C2 } C

 7.  INV and A { C1; C2; C4 } INV

 8.  INV { C5 } INV

 9.  PRE { C5 } POST

****************************************************************