public class AssertInduction {
	
	/**
	 * 
	 * @param n >= 1
	 * @return sum of pow(2,i) for i = 0 to n
	 */
	private int sumOfPows(int n){
		if (n==0) 
			return (int)Math.pow(2,0);
		else 
			return sumOfPows(n-1) + (int)Math.pow(2,n);
	}
	/**
	 * Check the following predicate: 
	 *      the sum of pow(2,i) for i = 0 to n == pow(2,n+1)-1
	 * @param n
	 */
	public void testSumOfPows(int n){
		if (n==0){
			// assert base case
			assert sumOfPows(0) == (int)Math.pow(2,1)-1 ;
			System.out.println("BASE CASE  pow(2,0) = pow(2,1)-1 = 1  OK");
		}
		else{
			// assert the recursive case
			assert sumOfPows(n) == (int)Math.pow(2,n+1)-1 ;
		    System.out.println(
		    "The sum of pow(2,i) for i = 0 to n  =  pow(2,n+1)-1 holds for n = " 
		     + n + ", and equals: " + sumOfPows(n));
		    
		}   
	}

	
	
	
	/**
	 * 
	 * @param n >= 1 n is the number of odds we add together
	 * @return sum of first n odds
	 */
	private int sumOfOdds(int n){
		if (n==1) 
			return n;
		else 
			return sumOfOdds(n-1) + 2*n-1;
	}
	/**
	 * Check the following predicate: 
	 *      the sum of the first n odds == n*n
	 * @param n
	 */
	public void testSumOfOdds(int n){
		if (n==1){
			// assert base case
			assert sumOfOdds(1) == 1;
			System.out.println("BASE CASE sum of first odd = 1  OK");
		}
		else{
			// assert the general case
			assert sumOfOdds(n) == n*n ;
		    System.out.println(
		    "The sum of first n odds = n*n holds for n = " 
		     + n + ", and equals: " + sumOfOdds(n));
		    
		}   
	}

	
	
	
	
	
	
	
	/**
	 * 
	 * @param n >= 0
	 * @return n!
	 */
	private int factorial(int n){
		if (n==0)
			return 1;
		else 
			return n*factorial(n-1);
	}
	
	/**
	 * 
	 * @param n >= 4
	 */
	public void testPowLessFact(int n){
		if(n==4){
			assert (int)Math.pow(2,4) < factorial(4);	
			System.out.println("BASE CASE  pow(2,4) = " + (int)Math.pow(2,4) +
					" < 4! = " + factorial(4) + " OK");			
		}else{	
		assert (int)Math.pow(2,n) < factorial(n);
		System.out.println("pow(2," +n+ ") = " +  (int)Math.pow(2,n) + 
				           " < " +n+ "! = " + factorial(n)  +"   OK");
		}
	}
	
	
	
	public static void main(String[] args) {

		AssertInduction a = new AssertInduction(); 
	    
		
	    System.out.println("Testing Sum of odds equals square predicate");	    
	    for(int i=1; i<12; i+=2)
	         a.testSumOfOdds(i);
		
		System.out.println("\n\nTesting sum of powers of 2 predicate");
		for(int i=0; i<10; i++)
	         a.testSumOfPows(i);
	
	    System.out.println("\n\nTesting power of 2 less factorial predicate");	    
	    for(int i=4; i<10; i++)
	         a.testPowLessFact(i);	  
			    	    
	}

}