Recursive Computation of Factorials

We revisit the computation of factorial numbers by discussing a directly recursive solution and an indirectly recursive solution.

The directly recursive solution implemented by a method fac0 is straight-forward:

  public static int fac0(int n) /*@
    requires VAR n >= 0 AND factorial(VAR n) <= Base.MAX_INT;
    ensures VALUE@NEXT = factorial(VAR n);
    decreases VAR n;
  @*/
  {
    if (n <= 0) return 1;
    int n0 = fac0(n-1);
    return n*n0;
  }

The specification is extended by a recursion measure, i.e., a term whose value must be decreased by every recursive invocation of that method.

If we switch to the “Semantics” view and select the method call int n0 = fac0(n-1), the following semantics is displayed:

The transition relation of that call is derived from the method’s postcondition: it says that the poststate s₂ of the method execution (next ~ s₂ indicates that this state has the same variable values as the poststate next of the method call) returns the value of factorial(n-1) which is stored in the variable n₀ (which is the only visible variable that is modified by the statement). Since every statement is only executed in a prestate now with property executes@now, the pre-state knowledge tells us that n is positive and factorial(n) is in the range of type int, as is required by the precondition of the method call.

From the transition relation of the method call, the transition relation of the whole method body can be derived:

We can clearly see two cases depending on the truth value of old n <= 0: if this is false, the second branch tells us that the method terminates by returning old n⋅factorial(old n-1); if this is true the first branch tells⁴ that the return value of the method is 1.

In the “Analysis” view, the following non-trivial verification tasks are displayed:

Among these, only the task for the postcondition and the preconditions require major human interaction. As for the proof of the postcondition, by some human guidance

Here it has to be shown (by appropriate instantiation of formula “1yj” derived from axiom fac_ax2 in theory Math) that factorial(n_old) = n_old ⋅factorial(n_old -1).

The proof of the preconditions essentially have to show that the argument of the recursive factorial call and the return value are in the range of type int; the detailed proofs are not difficult but a a bit tedious:

The RISC ProgramExplorer also supports arbitrary mutual recursion. As an example, take the following computation of the factorial numbers performed by two methods fac1 and fac2 which call each other:

  public static int fac1(int n) /*@
    requires VAR n >= 0 AND factorial(VAR n) <= Base.MAX_INT;
    ensures VALUE@NEXT = factorial(VAR n);
    decreases VAR n;
  @*/
  {
    if (n <= 0) return 1;
    int n0 = fac2(n-1);
    return n*n0;
  }

  public static int fac2(int n) /*@
    requires VAR n >= 0 AND factorial(VAR n) <= Base.MAX_INT;
    ensures VALUE@NEXT = factorial(VAR n);
    decreases VAR n;
  @*/
  {
    if (n <= 0) return 1;
    int n0 = fac1(n-1);
    return n*n0;
  }

The methods have the same state relations and verification tasks as the directly recursive method fac0; we thus omit the details.

4.2 Recursive Computation of Factorials