Write and verify a program that computes the sum of the squares of the n smallest positive odd integers. For example, when n is 4, the sum should be 1 + 9 + 25 + 49 == 84. Here is the specification:

Declarative interface:

const int n; /* n is the number of squares (input) */

int sum; /* the sum is stored in this variable */

Pre-condition: ASSERT( n >= 1 )

Post-condition: ASSERT( sum == ? n?1 i=0 (2*i+1)*(2*i+1) )

The program should use a while-loop and standard arithmetic operations. Select a loop invariant and give a complete proof tableau for the program (including all the intermediate assertions). Also make an argument for termination.