Proving correctness of a loop that calculates the sum of array

Question

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?