bench/infer/incr.mlw

   1 module Incr
   2
   3         use int.Int
   4         use int.MinMax
   5         use ref.Ref
   6         use ref.Refint
   7
   8         let incr1 [@infer] [@bddinfer] (x:int) : int
   9           ensures { result = max x 0 }
  10         = let i = ref 0 in
  11           while !i < x do
  12             variant { x - !i }
  13             incr i;
  14           done;
  15           !i
  16
  17         let incr3 [@infer:box] [@bddinfer] (x:int) : int
  18           ensures { result = max x 0 }
  19         = let i = ref 0 in
  20           while !i < x do
  21             variant { x - !i }
  22             incr i;
  23           done;
  24           !i
  25
  26 end