Recursion
Factorial

Document last modified: 
class Factorial {

   /*@ pre n >= 1;

          post n == 1 ==> \result == 1;
          post n > 1   ==> \result == n*Fac(n-1);
   @*/

   int Fac (int n) {
     if (n == 1) return 1;
     return n * Fac(n-1);
   }
}

Exercise

  1. What does the postconditions say in English?
     
  2. Why are two postconditions necessary?
     
  3. What is the implication of changing the postcondition to:

    post n == 1 ==> \result == 2;