#### 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.