Name __________________________
Given the following program, create appropriate loop invariants (statements that are true each time the program reaches the point labeled /* HERE */ in the code). You should have 4 invariants -- one for each of x, y, z, and i.
Once you have your four loop invariants, prove that they are really invariant by induction. Then, use the loop invariants to show that that the following function returns the cube of its argument, assuming that the input argument is non-negative.
Thus, you will need to prove two things: (1) that each loop invariant you've created holds true before every loop test and (2) that for the precondition N >= 0, the postcondition x = N*N*N holds (as long as N hasn't changed).
static long cube(long N)
{
long i, x, y, z;
x = 0;
y = 1;
z = 6;
for( i = 0; /* HERE */ i < N; i++ )
{
x = x + y;
y = y + z;
z = z + 6;
}
return x;
}