cvc4-models.mlw 550 Bytes
Newer Older
1
2
module M

David Hauzar's avatar
David Hauzar committed
3
  use import ref.Ref
4

David Hauzar's avatar
David Hauzar committed
5
  use import int.Int
6

David Hauzar's avatar
David Hauzar committed
7
8
9
10
11
12
13
  function projf (l : int) : int
  =
  l+100

  meta "model_projection" function projf

  val y "model" "model_projected" "model_trace:y" :ref int
14

David Hauzar's avatar
David Hauzar committed
15
  let incr ( x "model" "model_trace:x" : ref int ): unit
16
  ensures { !x = old !x + 2 + !y }
David Hauzar's avatar
David Hauzar committed
17
  = 
18
  y := !y + 1;	 
David Hauzar's avatar
David Hauzar committed
19
20
  x := !x + 1;
  x := !x + 1
21

David Hauzar's avatar
David Hauzar committed
22
23
24
25
  let test_loop ( x "model" "model_trace:x" : ref int ): unit
  ensures { !x < old !x }
  =
  incr x;
26
  while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
27
end