/* demonstration of assertions in action */

#include <cassert>
#include <iostream>


     int isqrt(int i);
     // pre: i == i0 and i0 >=0
     // post: n is returned where n*n <= i0 <(n+1)*(n+1)


int main()//unit tests for isqrt
{
	assert(isqrt(0)==0);
	assert(isqrt(1)==1);
	assert(isqrt(2)==1);
	assert(isqrt(3)==1);
	assert(isqrt(4)==2);

     for ( int i = 0; i<30; i++)
     {  int n = isqrt(i);
        assert( (n*n <= i) && (i <(n+1)*(n+1)));
     }
}

int isqrt(int i)
{ assert( i >=0 ); 
  //assert( (0*0 <= i ) && ( 1==(0+1)*(0+1) ) && ( 0 == 0));
  int n=0;
  //assert( (n*n <= i ) && ( 1==(n+1)*(n+1) ) && ( 0 == n));
  int s=1;
  //assert( (n*n <= i ) && ( s==(n+1)*(n+1) ) && ( 0 == n));
  //assert( (n*n <= i ) && ( s==(n+1)*(n+1) ) && ( 0 == 2*n));
  //assert( (n*n <= i ) && ( s==(n+1)*(n+1) ) && ( 1 == 2*n+1));
  int odd=1;
  //assert( (n*n <= i ) && ( s==(n+1)*(n+1) ) && ( odd == 2*n+1));
  while(s <=  i) // inv: ( n*n <= i ) && ( s==(n+1)*(n+1) ) && ( odd == 2*n+1)
  {
    //assert( (s <=  i ) && ( n*n <= i ) && ( s==(n+1)*(n+1) ) && ( odd == 2*n+1));
    //assert( (s <=  i ) && ( s == (n+1)*(n+1) ) && ( odd == 2*n+1));
    //assert( (s <=  i ) && ( s == (n+1)*(n+1) ) && ( odd+2 == 2*n+2+1));
    //assert( (s <=  i ) && ( s == (n+1)*(n+1) ) && ( odd+2 == 2*(n+1)+1));
	n=n+1;
    //assert( (s <=  i ) && ( s == n*n ) && ( odd+2 == 2*n+1));
	odd=odd+2;
    //assert( (s   <=  i ) && ( s == n*n ) && ( odd == 2*n+1));
    //assert( (n*n <=  i ) && ( s == n*n ) && ( odd == 2*n+1));
    //assert( (n*n <=  i ) && ( s+2*n+1 == n*n+2*n+1 ) && ( odd == 2*n+1));
    //assert( (n*n <=  i ) && ( s+odd==(n+1)*(n+1) ) && ( odd == 2*n+1));
	s=s+odd;
    //assert( (n*n <=  i ) && ( s==(n+1)*(n+1) ) && ( odd == 2*n+1));
  }
  //assert( (n*n <=  i ) && ( s==(n+1)*(n+1) ) && ( odd == 2*n+1 ) && !(s<=i));

  //assert( (n*n <=  i ) && ( i<(n+1)*(n+1)));
 return n;
}