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 == i2 ô i < n ô fd == 2*i+1 ô sd == 2
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 == i2 ô i < n ô fd == 2*i+1 ô sd == 2
sum = sum + fd;
fd = fd + sd;
i = i+1;
}
lAssert sum == n2
lThe
arrow-ed assertion is called a loop
invariant.
