## Various programs computing the factorial, in Why3

The following programs compute the factorial, in various ways.

**Authors:** Claude Marché / Jean-Christophe Filliâtre

**Topics:** Arithmetic

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

(* Various programs computing the factorial. *) module FactRecursive use int.Int use int.Fact let rec fact_rec (x:int) : int requires { x >= 0 } variant { x } ensures { result = fact x } = if x = 0 then 1 else x * fact_rec (x-1) let test0 () = fact_rec 0 let test1 () = fact_rec 1 let test7 () = fact_rec 7 let test42 () = fact_rec 42 end module FactImperative use int.Int use int.Fact use ref.Ref let fact_imp (x:int) : int requires { x >= 0 } ensures { result = fact x } = let y = ref 0 in let r = ref 1 in while !y < x do invariant { 0 <= !y <= x } invariant { !r = fact !y } variant { x - !y } y := !y + 1; r := !r * !y done; !r let test0 () = fact_imp 0 let test1 () = fact_imp 1 let test7 () = fact_imp 7 let test42 () = fact_imp 42 end

download ZIP archive