ref_mono.mlw 1.14 KB
Newer Older
1 2
module Ref

3
  type ref1 = { mutable contents [@model_trace:] : int }
4

5
  function (!) (x: ref1) : int = x.contents
6

7
  let ref1 (v: int) ensures { result = { contents = v } } = { contents = v }
8

9
  let (!) (r:ref1) ensures { result = !r } = r.contents
10

11
  let (:=) (r:ref1) (v:int) ensures { !r = v } = r.contents <- v
12 13 14 15 16 17 18 19

end

module M
  use list.List
  use int.Int
  use Ref

20
  let test_post (x: int) (y: ref1): unit
21 22 23 24
    ensures { old !y >= x }
      =
      y := x - 1 + !y

25
  let test_post2 (x: int) (y: ref1): unit
26 27 28 29 30 31 32 33 34
    requires { x > 42 }
    ensures { old !y > !y + x }
      =
      y := x - 1 + !y


  (**********************************************************
   ** Getting counterexamples for terms of primitive types **
   **********************************************************)
35
  val y :ref1
36

37
  let incr (x23: ref1): unit
38 39 40 41 42 43 44
  ensures { !x23 = old !x23 + 2 + !y }
  =
  (*#"random_path.random" 62 27 32#*)
  y := !y + 1;
  x23 := !x23 + 1;
  x23 := !x23 + 1

45
  let test_loop (x: ref1): unit
46 47 48 49 50 51 52 53 54 55 56 57
  ensures { !x < old !x }
  =
  label L in
  incr x;
  label M in
  while !x > 0 do
  invariant { !x > !x at L + !x at M }
  variant { !x }
    x := !x - 1
  done

end