How to construct and justify loop invariant, which allows to show partial correctness

I need to construct and justify a loop invariant with given specification:

{n > 0} P {q = | {j: a[j]=x and 0 <= j < n} |}

where |A| is a number of elements of set A. It means that q is equal to the number of elements from array a that are equal to x.

Code P is specified as:

{
int i = 0, q = 0;
while (i != n){
    if (a[i] == x)
        q = q + 1;
    i = i + 1;
}

I know that loop invariant must be true:

• before the loop starts
• before each iteration of the loop
• after the loop terminates

but I have no clue how should I find the right loop invariant, that would allow me to show partial correctness of P afterwards. I already tried to look at every single iteration of the loop and variables for random n, x and a[0...n-1] to see which values combined are constant while the loop is working, but it did not help.

Look at your code carefully. At the beginning, q is 0, and it only grows when you find new elements that are == x. So

q = | {j: a[j]=x and 0 <= j < i} |

is part of your invariant. Note that in your specification, you had < n instead of < i. Notice also that, at loop termination, i == n. So it will also be valid at the start. It will also be true at any point in between: so far, so good. Is anything else missing? Yes, we should also state that

0 <= i <= n -- because that describes the range of values of i (otherwise, i would be free to venture outside the array).

Is this all? Yes -- there is no other loop state left to describe. Therefore, your complete invariant looks like

q = | {j: a[j]=x and 0 <= j < i} | and 0 <= i <= n

When solving these exercises, you can try these 2 steps:

• try to describe in plain text what goes on in the algorithm: "I sweep i from 0 to n-1, stopping at n, and at every moment, I keep in q the amount of x that I have found within the array". All variables involved in the loop must be mentioned!.
• translate that plain text into math, while also making sure that your post-condition is reflected in the invariant, generally replacing the n by the loop counter (in this case, i)

As a thought experiment, try to write the invariant with the equivalent loop (but iterating from the end to the beginning) instead:

{
int i = n-1, q = 0;
while (i >= 0){
    if (a[i] == x)
        q = q + 1;
    i = i - 1;
}

Mouse over for answer (but try to figure it out first).

q = | {j: a[j]=x and i < j < n} | and -1 <= i < n Note the different limits, reflecting that i sweeps differently; but the same overall structure