# Proving correctness of a loop that calculates the sum of array

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?

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]$$

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.