Introduction to Programming in ATS:
<<< PreviousProgramming with Theorem-ProvingNext >>>

Example: Another Verified Factorial Implementation

The function ifact presented in the section on specifying with enhanced precision is a verified implementation of the factorial function as its type guarantees that ifact implements the specification of factorial encoded by the dataprop FACT. Clearly, the implementation of ifact closely follows the declaration of FACT. If we think of the latter as a logic program, then the former is essentially a functional version extracted from the logic program. However, the implementation of a specification in practice can often digress far from the specification algorithmically. For instance, we may want to have a verified implementation of factorial that is also tail-recursive. This can be done as follows: 

fun ifact2 {n:nat} .<>.
  (n: int n): [r:int] (FACT (n, r) | int r) = let
  fun loop
    {i:nat | i <= n} {r:int} .<n-i>. (
    pf: FACT (i, r) | n: int n, i: int i, r: int r
  ) : [r:int] (FACT (n, r) | int r) =
    if n - i > 0 then let
      val (pfmul | r1) = (i+1) imul2 r in loop (FACTind (pf, pfmul) | n, i+1, r1)
    end else (pf | r) // end of [if]
  // end of [loop]
in
  loop (FACTbas () | n, 0, 1)
end // end of [ifact2]

The function ifact2 is assigned a type indicating that ifact2 is a verified implementation of factorial, and it is defined as a call to the inner function loop that is clearly tail-recursive. If we erase types and proofs, the function ifact2 is essentially defined as follows: 

fun ifact2 (n) = let
  fun loop (n, i, r) =
    if n - i > 0 then let
      val r1 = (i+1) * r in loop (n, i+1, r1)
    end else r
  // end of [loop]
in
  loop (n, 0, 1)
end // end of [ifact2]

When the inner function loop is called on three arguments n, i and r, the precondition for this call is that i is natural number less than or equal to n and r equals fact(i), that is, the value of the factorial function on i. This precondition is captured by the type assigned to loop and thus enforced at each call site of loop in the implementation of ifact2.

Please find on-line the entirety of the above presented code plus some testing code.

<<< PreviousHomeNext >>>
Specifying with Enhanced PrecisionUpExample: Verified Fast Exponentiation