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 > nWe also want the post conditionj = 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? 
Proving correctness of a loop that calculates the sum of array
loops;loop invariants;program correctness
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.