Commit 739714d4 authored by MARCHE Claude's avatar MARCHE Claude

Experiments with Alt-Ergo models

parent 0fb98676
(*
DONE alt-ergo devrait tenir que de certains labels, i.e.
pour les termes et les propositions, un label qui matche "model:.*", et
pour les variables "model:[0-9]+"
TODO: modele donné apres timeout
*)
module M1
use import int.Int
let f (x "0":int) : int =
{ }
let f (x "model:0":int) : int =
{ }
if ("model:cond" x >= 42) then x + 3 else 0
{ "model:post" result <= 50 }
let f_no_lab (x:int) : int =
{ }
if x >= 42 then x + 3 else 0
{ result <= 50 }
use import module ref.Ref
let g (x "0": ref int) : int =
{ }
let g (x "model:0": ref int) : int =
{ }
x := !x + 1;
if !x >= 42 then !x + 3 else 0
if ("model:cond" !x >= 42) then !x + 3 else 0
{ "model:post" result <= 50 }
let g_no_label (x : ref int) : int =
{ }
x := !x + 1;
if (!x >= 42) then !x + 3 else 0
{ result <= 50 }
end
(*
Local Variables:
compile-command: "../../bin/why3ide alt-ergo-models.mlw"
End:
*)
theory T1
theory T
use import int.Int
goal G : forall x "1":int. ("cond" x >= 42) -> x + 3 <= 50
goal g_no_lab : forall x:int. x >= 42 -> x + 3 <= 50
goal g_lab0 : forall x "model:0":int. ("model:cond" x >= 42) ->
("model:concl" x + 3 <= 50)
goal g_lab1 : forall x "model:1":int. ("model:cond" x >= 42) ->
("model:concl" x + 3 <= 50)
constant x : int
goal g2_lab : forall y "model:0":int. ("model:concl" x >= y)
end
theory T2
theory ModelInt
use import int.Int
use import int.Int
constant x : int
goal test0 : forall x "model:0":int. not (0 < x < 1)
goal test1 : forall x "model:0":int. not (0 <= x <= 1)
use import int.EuclideanDivision
goal test2 : forall x "model:0":int. div x x = 1
goal test_overflow:
forall x "model:0" y "model:0" : int.
0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535
goal test_overflow2:
forall x "model:0" y "model:0" : int.
-2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535
predicate is_int16 (x:int) = -65536 <= x <= 65535
goal test_overflow_int16:
forall x "model:0" y "model:0" : int.
is_int16 x /\ is_int16 y -> is_int16 (x + y)
goal test_overflow_int16_alt:
forall x "model:0" y "model:0" : int.
-65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535
goal g : forall y:int. x >= y
goal test_overflow_int16_bis:
forall x "model:0" y "model:0" : int.
is_int16 x /\ is_int16 y /\ 0 <= x <= y -> is_int16 (x + y)
predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647
goal test_overflow_int32:
forall x "model:0" y "model:0" : int.
is_int32 x /\ is_int32 y -> is_int32 (x + y)
goal test_overflow_int32_bis:
forall x "model:0" y "model:0" : int.
is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)
end
theory ModelReal
use import real.Real
goal test1 : forall x "model:0":real. not (0.0 < x < 1.0)
goal test2 : forall x "model:0":real. x/x=1.0
end
theory ModelArray
use import map.Map
goal t1 : forall t "model:0" :map int int, i "model:0" : int.
get (set t 0 42) i = get t i
end
......@@ -233,11 +233,11 @@ let load_config config original_config =
*)
let debug_save_config n c =
let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
prover_altern = "" } in
let p = Mprover.find coq (get_provers c) in
let time = Whyconf.timelimit (Whyconf.get_main c) in
Format.eprintf "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
Format.eprintf "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
n time p.editor
let save_config t =
......@@ -730,7 +730,7 @@ let editors_page c (notebook:GPack.notebook) =
let editors = Whyconf.get_editors c.config in
let _,strings,indexes,map =
Meditor.fold
(fun k data (i,str,ind,map) ->
(fun k data (i,str,ind,map) ->
let n = data.editor_name in
(i+1, n::str, Meditor.add k i ind, Meditor.add n k map))
editors (2, [], Meditor.empty, Meditor.empty)
......@@ -754,11 +754,11 @@ let editors_page c (notebook:GPack.notebook) =
match combo#active_iter with
| None -> ()
| Some row ->
let data =
let data =
match combo#model#get ~row ~column with
| "(default)" -> ""
| s ->
try Meditor.find s map
| s ->
try Meditor.find s map
with Not_found -> assert false
in
(* Format.eprintf "prover %a : selected editor '%s'@." *)
......@@ -1004,7 +1004,8 @@ let replace_prover c to_be_removed to_be_copied =
res
*)
let read_config conf_file extra_files = read_config conf_file extra_files; init ()
let read_config conf_file extra_files =
read_config conf_file extra_files; init ()
(*
Local Variables:
......
......@@ -186,9 +186,9 @@ and print_fmla_node info fmt f = match f.t_node with
(print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
f1 (print_fmla info) f3
| Tlet _ -> unsupportedTerm f
"alt-ergo : you must eliminate let in formula"
"alt-ergo: you must eliminate let in formula"
| Tcase _ -> unsupportedTerm f
"alt-ergo : you must eliminate match"
"alt-ergo: you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt =
......
......@@ -243,7 +243,7 @@ let quantify env rm sreg f =
in
let id = Spv.fold test vars None in
(**)
let label = Slab.singleton (create_label "0") in
let label = Slab.singleton (create_label "model:0") in
(**)
let id = id_clone ~label (def_option r.R.r_tv.tv_name id) in
let r' = create_vsymbol id (purify r.R.r_ty) in
......@@ -490,6 +490,8 @@ and wp_desc env rm e q = match e.expr_desc with
| Eif (e1, e2, e3) ->
let res = v_result e1.expr_type in
let test = t_equ (t_var res) (t_True env) in
let label = Slab.singleton (create_label "model:cond") in
let test = t_label ~loc:e1.expr_loc label test in
(* if both branches are pure, do not split *)
let q1 =
try
......
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