Synthesis of Squaring Program
lAssert n > 0 is the number to be squared.
lint sum = 0; // accumulated sum
int i = 0; // step number
int fd = 1; // first difference
int sd = 2; // second difference
while( i < n )
{
sum = sum + fd;
fd = fd + sd;
i = i+1;
}
int i = 0; // step number
int fd = 1; // first difference
int sd = 2; // second difference
while( i < n )
{
sum = sum + fd;
fd = fd + sd;
i = i+1;
}
lAssert sum == n2
lWhat/where
to add intermediate assertions?