bench/check-ce/loop_inv_int_mono.mlw

   1
   2 module M
   3
   4 use int.Int
   5
   6 type t = { mutable c : int }
   7
   8 let f () : unit
   9   diverges
  10   =
  11   let a = { c = 0 } in
  12   a.c <- 1;
  13   let b = { c = 2 } in
  14   while b.c < 10 do
  15     invariant { b.c < a.c + 5 }
  16     b.c <- a.c + b.c
  17   done
  18
  19 end
  20
  21 module N
  22
  23 use int.Int
  24
  25 type t = { mutable c : int }
  26
  27 val a : t
  28
  29 val b : t
  30
  31 let f () : int
  32   diverges
  33   ensures { result < a.c }
  34   =
  35   a.c <- 1;
  36   b.c <- 2;
  37   while b.c < 10 do
  38     invariant { b.c < a.c + 5 }
  39     b.c <- a.c + b.c
  40   done;
  41   b.c
  42
  43 end