0
$\begingroup$

I am trying to mathematically prove that the following program is correct:

int ArraySumC(int[] a) {
    int i = 0;
    int j = 0;

    while (i <= n) {
        j = j + a[i];
        i = i + 1;
    }

    return j;
}

When the loop ends, we want the invariant, Q, and the condition for loop termination, B'.

Q ∧ B' = Q ∧ i > n

We also want the post condition

j = sum(a[1] ... a[n])

I'm not sure how to go from here, because I don't know what Q should be. I am used to B' being an equality and thus being able to substitute one side of B' into the post condition. Should I assume that B' is i = n + 1? Or is there another way to deal with the inequality?

$\endgroup$
3
$\begingroup$

I think your postcondition is wrong. Since index i is initialized at 0, you're actually summing from 0 to n, not from 1 to n. The postcondition, lets call it $P$, should be:

$$ j = \sum_{k=0}^{n} a[k] $$

Or:

j = sum(a[0] ... a[n])

Usually you would write $B$ as $i \neq n+1$ instead of $i \le n$, because it makes the proof easier. In that case, you would choose $Q$ as (assuming array indexing starts at 0):

$$ j = \sum_{k=0}^{i-1} a[k] $$

Or in your notation:

j = sum(a[0] ... a[i-1])

Then $ Q \land \lnot B \implies P$ is true because you can substitute $i$ by $n+1$. Of course, you would have to prove that $Q$ is a valid invariant, but I'll leave that to you.

In your case,$\lnot B$ is $i>n$ instead of $i = n + 1$, so you can't use substitution. You can deal with the inequality by adding information to the invariant and then proving $i = n +1$ using this new information. Our new invariant $Q'$ could be:

$$Q \land i \le n+1$$

This new condition holds before the loop starts because $i$ starts at 0 and $n+1$ must be at least $1$.To prove that $Q'$ is a valid invariant, we have to show that it also holds after every iteration. Each time the loop executes $i$ changes to $i+1$, so we must prove that $ i+1 \le n+1$, which is true because the loop condition states that $i \le n$ was true when the iteration started.

Now we know that $Q \land i \le n + 1 \land i > n$ holds after the loop ends. And since $i \le n + 1 \land i > n \implies i = n + 1$ and $Q \land i = n + 1 \implies P$, the program is correct.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.