What is the loop invariant for a summation of cubes algorithm?

Question

I'm not 100% sure what the invariant in a triple power summation is.

Note: n is always a non-negative value.

Pseudocode:

triplePower(n)
    i=0
    tot=0
    while i <= n LI1
        j = 0
        while j < i LI2
            k = 0
            while k < i LI3
                tot = tot + i
                k++
            j++
        i++

I know its messy and could be done in a much easier way, but this is what I am expected to do (mainly for algorithm analysis practice).

I am to come up with three loop invariants; LI1, LI2, and LI3.
I'm thinking that for LI1 the invariant has something to do with tot=(i^2(i+1)^2)/4 (the equation for a sum a cubes from 0 to i)
I don't know what to do for LI2 or LI3 though. The loop at LI2 make i^3 and LI3 makes i^2, but I'm not totally sure how to define them as loop invariants.

Would the invariants be easier to define if I had 3 separate total variables in each of the while loop bodies that added to a main total right before i++ in the first loop?

Thanks for any help you can give.

Answer 1

I think you can define them as below:

LI1 <= (i^2(i+1)^2)/4
LI2 <= (i+1)^3 + (i^2(i+1)^2)/4
LI3 <= (i+1)^2 + i^3 + (i^2(i+1)^2)/4

(if your calculated amounts is right).