examples/fact_vc_sp.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   = [@vc:sp]
  14     if x = 0 then 1 else x * fact_rec (x-1)
  15
  16   let test0 () = fact_rec 0
  17   let test1 () = fact_rec 1
  18   let test7 () = fact_rec 7
  19   let test42 () = fact_rec 42
  20
  21 end
  22
  23 module FactImperative
  24
  25   use int.Int
  26   use int.Fact
  27   use ref.Ref
  28
  29   let fact_imp (x:int) : int
  30     requires { x >= 0 }
  31     ensures { result = fact x }
  32   = [@vc:sp]
  33     let y = ref 0 in
  34     let r = ref 1 in
  35     while !y < x do
  36       invariant { 0 <= !y <= x }
  37       invariant { !r = fact !y }
  38       variant { x - !y }
  39       y := !y + 1;
  40       r := !r * !y
  41     done;
  42     !r
  43
  44   let test0 () = fact_imp 0
  45   let test1 () = fact_imp 1
  46   let test7 () = fact_imp 7
  47   let test42 () = fact_imp 42
  48
  49 end