ref.mlw 1.02 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
module M
  use import ref.Ref
  use import list.List
  use import int.Int

  type int_type = Integer int

  goal G : forall x "model" : int_type. match x with Integer y -> y > 0 end

  let test_post (x "model" "model_trace:x" : int) (y "model" "model_trace:y" : ref int): unit
    ensures { "model_vc_post" old !y >= x }
      =
      y := x - 1 + !y

  (**********************************************************
   ** Getting counterexamples for terms of primitive types **
   **********************************************************)
  val y "model" "model_trace:y" :ref int

  let incr ( x23 "model" "model_trace:x23" : ref int ): unit
  ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
  =
  (*#"random_path.random" 62 27 32#*)
  y := !y + 1;
  x23 := !x23 + 1;
  x23 := !x23 + 1

  let test_loop ( x "model" "model_trace:x" : ref int ): unit
  ensures { "model_vc_post" !x < old !x }
  =
31 32 33 34 35
  label L in
  incr x;
  label M in
  while !x > 0 do
  invariant { "model_vc" !x > !x at L + !x at M }
36 37 38 39 40
  variant { !x }
    x := !x - 1
  done

end