Commit 048d5150 authored by David Hauzar's avatar David Hauzar

Counterexample examples - refactored, polished, completed.

parent baac0c6b
......@@ -5,45 +5,10 @@ module M
type int_type = Integer int
function projfi "model_trace:.projfi" (l : int) : int
meta "inline : no" function projfi
meta "model_projection" function projfi
function projfl "model_trace:.projfl" (l : list int_type) : int
=
match l with
| Nil -> 0
| Cons (Integer n) _ -> n
| _ -> 0
end
function projf1 "model_trace:.projf1" (l : int) : bool
=
l > 0
function projf2 "model_trace:.projf2" (l : int) : bool
=
l <= 0
meta "inline : no" function projfl
meta "model_projection" function projfl
meta "inline : no" function projf1
meta "model_projection" function projf1
meta "inline : no" function projf2
meta "model_projection" function projf2
val y "model_projected" "model" "model_trace:y" :ref int
let proj_test ( l "model_projected" : list int_type) : int
ensures { result > 0 }
=
match l with
| Nil -> 1
| Cons (Integer n) _ -> n
| _ -> 1
end
(**********************************************************
** 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" "model_func" !x23 = old !x23 + 2 + !y }
......@@ -59,20 +24,50 @@ module M
incr x;
while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
(**************************************
** Getting counterexamples for maps **
**************************************)
use import map.Map
let test_map (x "model" : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
ensures { "model_vc" !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let test_map2 (x "model" : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
let test_map_multidim1 (x "model" : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
type r = {f:int; g:bool}
let test_record1 (x "model" "model_trace:x" : r) : int
let test_map_multidim2 (x "model" : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
=
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
x := Map.set !x 0 x0
(*****************************************
** Getting counterexamples for records **
*****************************************)
(*** In all cases, records are decomposed using match eval ***)
type r = {f "field_f" :int; g:bool}
(* Projection functions *)
function projf_r_f "model_trace:.f" (x : r) : int
=
x.f
function projf_r_g "model_trace:.g" (x : r) : bool
=
x.g
meta "inline : no" function projf_r_f
meta "model_projection" function projf_r_f
meta "inline : no" function projf_r_g
meta "model_projection" function projf_r_g
let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
ensures { "model_vc" "model_func" result = 1 }
=
if x.g then
......@@ -80,23 +75,131 @@ module M
else
1
let test_record2 (x "model" "model_trace:x" : ref r) : unit
let record_match_eval_test2 (x "model_projected" : r ) : int
ensures { result = 1 }
=
x.f
let record_match_eval_test3 (x "model" "model_trace:x" : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
let test_record3 (x "model" "model_trace:x" : ref r) : r
let record_match_eval_test4 (x "model" "model_trace:x" : ref r) : r
ensures { "model_vc" "model_func" result.g }
=
x := { !x with f = 6 };
!x
val re "model" : ref r
val re "model_projected" : ref r
let test_record4 (x "model" "model_trace:x" : ref r) : r
let test_record_match_eval_test5 (x "model" "model_trace:x" : ref r) : r
ensures { "model_vc" "model_func" result = !re }
=
x := { !x with f = 6 };
!x
(***********************************************************
** Getting counterexamples for records and maps together **
***********************************************************)
(*** Records and maps together ***)
type r_map = {f_map:map bool int; g_bool:bool}
function projf_r_map_f_map "model_trace:.f_map" (rec_map : r_map) : map bool int
=
rec_map.f_map
function projf_r_map_g "model_trace:.g_map" (rec_map : r_map) : bool
=
rec_map.g_bool
meta "inline : no" function projf_r_map_f_map
meta "model_projection" function projf_r_map_f_map
meta "inline : no" function projf_r_map_g
meta "model_projection" function projf_r_map_g
(* Tests *)
(* Warning: does not terminate *)
let map_record_proj_test1 (map_rec "model_projected" : map bool r)
ensures { result = 0 }
=
map_rec[true].f
let record_map_proj_test2 (rec_map "model_projected" : r_map)
ensures { result = 0 }
=
rec_map.f_map[true]
val re_rec_map "model_projected" : r_map
let record_map_proj_test3 (rec_map "model_projected" : r_map)
ensures { result = re_rec_map }
=
rec_map
(*******************************************
** Definitions of projections used below **
*******************************************)
function projfi "model_trace:.projfi" (l : int) : int
= l
meta "inline : no" function projfi
meta "model_projection" function projfi
function projf1 "model_trace:.projf1" (l : int) : bool
=
l > 0
function projf2 "model_trace:.projf2" (l : int) : bool
=
l <= 0
meta "inline : no" function projf1
meta "model_projection" function projf1
meta "inline : no" function projf2
meta "model_projection" function projf2
(*******************************************************
** Getting counterexamples for maps with projections **
******************************************************)
(* Both indices and range of map will be projected using
projfi, projf1, and projf2
Warning: cvc4 is not able to handle projections there *)
let proj_map_test1 (x "model_projected" : ref (map int int)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* No projection function for bool -> the array should be
present in counterexample as it is. *)
let proj_map_test2 (x "model_projected" : ref (map int bool)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
=
x := Map.set !x 0 true
(*********************************
** Non-terminating projections **
*********************************)
(* Warning: if definition of the following projections are present,
the proof of everything below will not terminate. *)
function projfl "model_trace:.projfl" (l : list int_type) : int
=
match l with
| Nil -> 0
| Cons (Integer n) _ -> n
| _ -> 0
end
meta "inline : no" function projfl
meta "model_projection" function projfl
(* list int_type will be projected using projfl to int,
int will be projected using projfi, projf1, and projf2
Warning: does not terminate. *)
let proj_test ( l "model_projected" : list int_type) : int
ensures { result > 0 }
=
match l with
| Nil -> 1
| Cons (Integer n) _ -> n
| _ -> 1
end
end
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