Reading material

Pages 132-139.

Additional material

The Hoare triple
    { true } a[a[2]] = 1; { a[a[2]] = 1 }
is not valid. Consider an initial state such that a[1] = 2 and a[2] = 2. In the corresponding final state, a[1] = 2 and a[2] = 1, and therefore a[a[2]] = a[1] = 2.

Partial correctness

    { p } s { q }
if p holds before the execution of s and the execution of s terminates, then q holds afterwards.

Total correctness

    [ p ] s [ q ]
if p holds before the execution of s, then the execution of s terminates and q holds afterwards.

Question

Consider the following code fragment.
    i = 1;
    f = 1;
    while (i != n)
    {
        f = f * i;
        i = i + 1;
    }
The precondition is { n > 0 } and the postcondition is { f = n! }. Come up with a loop invariant and try to verify the above code fragment.