bench/check-ce/loop_ce.mlw

   1
   2 module M1
   3
   4 use int.Int
   5
   6 let ref a = 0
   7
   8 let ref b = 0
   9
  10 let f () =
  11   a <- -1;
  12   a <- 1;
  13   b <- 2;
  14   while b < 10 do
  15     variant { 10 - b }
  16     invariant { b - a < 5 }
  17     b <- b + a;
  18   done
  19
  20 end
  21
  22 module M2
  23
  24 use int.Int
  25
  26 let g (ref a: int)
  27   ensures { a = old a + 1 }
  28 =
  29   label X in
  30   if a <> 10 then a <- a + 1;
  31   assert { a = a at X }
  32
  33 end