Commit 2202577b authored by David Hauzar's avatar David Hauzar
Browse files

Counterexample examples updated.

parent 3e839ee4
......@@ -10,7 +10,7 @@ module M
meta "model_projection" function projf
val y "model" "model_projected" "model_trace:y" :ref int
val y "model_projected" "model_trace:y" :ref int
let incr ( x "model" "model_trace:x" : ref int ): unit
ensures { !x = old !x + 2 + !y }
......@@ -24,4 +24,18 @@ module M
=
incr x;
while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
use import map.Map
let test_map (x "model" "model_trace:x" : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
type r = {f:int; g:bool}
let test_record (x "model" "model_trace:x" : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment