Consider the C++
code for your algorithm:
max = a[0]; ind = 0;
for (int i = 1; i < n; i++)
{
if (a[i] > max)
{
max = a[i];
ind = i;
}
}
For the above algorithm, we would have:
- StateSpace = (a : N*, n : N, ind : N, max : N)
- Pre-condition = (a = a' /\ n = length(a))
- Post-condition = (Pre-condition /\ (max, ind) = MAX(i = 0, n) a[ i ])