bench/infer/logic_def.mlw

   1
   2 use int.Int
   3
   4 function succ (n : int) : int = n + 1
   5
   6 val incr (ref x : int) : unit
   7   writes { x }
   8   ensures { x = succ (old x) }
   9
  10 let f [@bddinfer] [@infer] () : unit =
  11   let ref a = 0 in
  12   while a <= 100 do
  13     variant { 100 - a }
  14     incr a
  15   done;
  16   assert { a = 101 }