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