ref.mlw 1.01 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 31 32 33 34 35 36 37 38
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 }
  =
  'L: incr x;
  'M: while !x > 0 do
  invariant { "model_vc" !x > at !x 'L + at !x 'M }
  variant { !x }
    x := !x - 1
  done

end