Commit d64f9981 authored by David Hauzar's avatar David Hauzar

Update examples for counterexample generation.

parent 1628b802
...@@ -5,6 +5,13 @@ module M ...@@ -5,6 +5,13 @@ module M
type int_type = Integer 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 ** ** Getting counterexamples for terms of primitive types **
**********************************************************) **********************************************************)
...@@ -19,11 +26,11 @@ module M ...@@ -19,11 +26,11 @@ module M
x23 := !x23 + 1 x23 := !x23 + 1
let test_loop ( x "model" "model_trace:x" : ref int ): unit let test_loop ( x "model" "model_trace:x" : ref int ): unit
ensures { !x < old !x } ensures { "model_vc_post" !x < old !x }
= =
incr x; 'L: incr x;
while "model" "model_trace:cond" !x > 0 do 'M: while !x > 0 do
invariant { !x >= 0 } invariant { "model_vc" !x > at !x 'L + at !x 'M }
variant { !x } variant { !x }
x := !x - 1 x := !x - 1
done done
......
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