bench/check-ce/for1_mono.mlw

   1 use int.Int
   2
   3 type t = { mutable c : int }
   4
   5 let f ()
   6   ensures { result = 2 }
   7 = let x = { c = 0 } in
   8     for i = 0 to 1 do
   9       invariant { x.c >= 0 }
  10       x.c <- x.c + 1
  11     done;
  12     x.c
  13
  14 (*
  15 counterexamle: `x = 0`, `i = 2` at beggining of loop.
  16
  17 The execution of `f` with the counterexample:
  18 - terminates normally if executed concretly;
  19 - terminates in error if executed abstractly (postcondition fails)
  20
  21 It is a real counterexample due to underspecification (weak loop
  22 invariant).
  23 *)