Back to slide -- Keyboard shortcut: 'u'  previous -- Keyboard shortcut: 'p'        Annotated program -- Keyboard shortcut: 't'    factorial/fac4.cs - An iterative Factorial function with a precondition - not C# 3.0.Lecture 9 - slide 5 : 30
Program 2

  public static BigInteger Factorial(int n){
    require n >= 0;                                 
    BigInteger res = 1;                             
    for(int i = 1; i <= n; i++)                     
      res = res * i;
    return res;
    ensure res = n * n-1 * ... * 1;  
  }