Proving correctness of a loop that calculates the sum of array
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&gt;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 &gt; n$ holds after the loop ends. And since $i \le n + 1 \land i &gt; n \implies i = n + 1$ and $Q \land i = n + 1 \implies P$, the program is correct.