bench/check-ce/loop_inv_int.mlw

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