bench/check-ce/while1_mono.mlw

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