ref.mlw 864 Bytes
Newer Older
1
module M
2 3 4
  use ref.Ref
  use list.List
  use int.Int
5

Guillaume Melquiond's avatar
Guillaume Melquiond committed
6 7
  let test_post (x: int) (y: ref int): unit
    ensures { old !y >= x }
8 9 10
      =
      y := x - 1 + !y

Guillaume Melquiond's avatar
Guillaume Melquiond committed
11 12 13
  let test_post2 (x: int) (y: ref int): unit
    requires { x > 42 }
    ensures { old !y > !y + x }
14 15 16
      =
      y := x - 1 + !y

17

18 19 20
  (**********************************************************
   ** Getting counterexamples for terms of primitive types **
   **********************************************************)
21
  val y :ref int
22

Guillaume Melquiond's avatar
Guillaume Melquiond committed
23
  let incr (x23: ref int): unit
24
  ensures { !x23 = old !x23 + 2 + !y }
25 26 27 28 29 30
  =
  (*#"random_path.random" 62 27 32#*)
  y := !y + 1;
  x23 := !x23 + 1;
  x23 := !x23 + 1

Guillaume Melquiond's avatar
Guillaume Melquiond committed
31
  let test_loop (x: ref int): unit
32
  ensures { !x < old !x }
33
  =
34 35 36 37
  label L in
  incr x;
  label M in
  while !x > 0 do
Guillaume Melquiond's avatar
Guillaume Melquiond committed
38
  invariant { !x > !x at L + !x at M }
39 40 41 42 43
  variant { !x }
    x := !x - 1
  done

end