/* 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) ) && ( 1 == 2*0+1));
  int n=0;
  //assert( ( n*n <= i ) && ( 1==(n+1)*(n+1) ) && ( 1 == 2*n+1));
  int s=1;
  //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( ( (n+1)*(n+1) <= i ) && ( s==(n+1)*(n+1) ) && ( odd  == 2*n+1));
	  //assert( ( (n+1)*(n+1) <= i ) && ( s==(n+1)*(n+1) ) && ( odd +2 == 2*(n+1)+1));
	n=n+1;
	  //assert( ( n*n <= i ) && ( s==n*n ) && ( odd +2 == 2*n+1));
	odd=odd+2;
	  //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( !(s<=i) && ( n*n <= i ) && ( s==(n+1)*(n+1) ) && ( odd == 2*n+1));
  //assert( !(s<=i) && ( n*n <= i ) && ( s==(n+1)*(n+1) ) );
  //assert( (s>i) && ( n*n <= i ) && ( s==(n+1)*(n+1) ) );
  //assert( ((n+1)*(n+1)>i) && ( n*n <= i ) && ( s==(n+1)*(n+1) ) );
  //assert( ((n+1)*(n+1)>i) && ( n*n <= i ) );

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