examples/fact.mlw

   1
   2 (* Various programs computing the factorial. *)
   3
   4 module FactRecursive
   5
   6   use int.Int
   7   use int.Fact
   8
   9   let rec fact_rec (x:int) : int
  10     requires { x >= 0 }
  11     variant  { x }
  12     ensures  { result = fact x }
  13   = if x = 0 then 1 else x * fact_rec (x-1)
  14
  15   let test0 () = fact_rec 0
  16   let test1 () = fact_rec 1
  17   let test7 () = fact_rec 7
  18   let test42 () = fact_rec 42
  19
  20 end
  21
  22 module FactImperative
  23
  24   use int.Int
  25   use int.Fact
  26   use ref.Ref
  27
  28   let fact_imp (x:int) : int
  29     requires { x >= 0 }
  30     ensures { result = fact x }
  31   = let y = ref 0 in
  32     let r = ref 1 in
  33     while !y < x do
  34       invariant { 0 <= !y <= x }
  35       invariant { !r = fact !y }
  36       variant { x - !y }
  37       y := !y + 1;
  38       r := !r * !y
  39     done;
  40     !r
  41
  42   let test0 () = fact_imp 0
  43   let test1 () = fact_imp 1
  44   let test7 () = fact_imp 7
  45   let test42 () = fact_imp 42
  46
  47 end