Commit 705f045b authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

vacid-0 benchmark in programs/vacid...

parent 0b18ac43
......@@ -252,7 +252,7 @@ clean::
# test target
%: %.mlw bin/whyml.byte
bin/whyml.byte -P alt-ergo $*.mlw
bin/whyml.byte -P alt-ergo --debug $*.mlw
###############
# proof manager
......
{
use array.ArrayLength as A
logic maxlen : int = 1000
type elt
logic default : elt
logic c1 : elt
logic c2 : elt
type 'a array = 'a A.t
logic (#)(a : 'a array, i : int) : 'a = A.select(a, i)
type sparse_array =
elt array * int array * int array * int (*sz*) * int (*n*)
logic sa_val (a : sparse_array) : elt array = let (val, _, _, _, _) = a in val
logic sa_idx (a : sparse_array) : int array = let (_, idx, _, _, _) = a in idx
logic sa_back(a : sparse_array) : int array = let (_, _, b, _, _) = a in b
logic sa_sz (a : sparse_array) : int = let (_, _, _, sz, _) = a in sz
logic sa_n (a : sparse_array) : int = let (_, _, _, _, n) = a in n
logic model(a : sparse_array, i : int) : elt =
let (val, idx, back, _, n) = a in
if 0 <= idx#i < n and back#(idx#i) = i then
val#i
else
default
logic invariant(a : sparse_array) =
let (val, idx, back, sz, n) = a in
0 <= n <= sz <= maxlen and
forall i : int. 0 <= i < n ->
0 <= back#i < sz and
idx#(back#i) = i
}
(*
parameter create :
sz:int ->
{ 0 <= sz <= maxlen }
sparse_array ref
{ sa_sz(!result) = sz and forall i:int. model(!result, i) = default }
*)
(* BUG
parameter malloc : n:int -> {} 'a array { A.length(result) = n }
*)
parameter malloc_elt : n:int -> {} elt array { A.length(result) = n }
parameter malloc_int : n:int -> {} int array { A.length(result) = n }
let create sz =
{ 0 <= sz <= maxlen }
ref ((malloc_elt sz, malloc_int sz, malloc_int sz, sz, 0) : sparse_array)
{ invariant(!result) and
sa_sz(!result) = sz and forall i:int. model(!result, i) = default }
let test a i =
{ 0 <= i < sa_sz(!a) }
let idx = sa_idx !a in
let back = sa_back !a in
let n = sa_n !a in
if 0 <= A.select idx i then
if A.select idx i < n then
A.select back (A.select idx i) = i
else
False
else
False
{ let (val, idx, back, sz, n) = !a in
result=True <-> (0 <= idx#i < n and back#(idx#i)=i) }
(*
parameter get :
a:sparse_array ref -> i:int ->
{ 0 <= i < sa_sz(!a) }
elt reads a
{ result = model(!a, i) }
*)
let get a i =
{ 0 <= i < sa_sz(!a) and invariant(!a) }
let val = sa_val !a in
if test a i then
A.select val i
else
default
{ result = model(!a, i) }
(*
parameter set :
a:sparse_array ref -> i:int -> v:elt ->
{ 0 <= i < sa_sz(!a) and invariant(!a) }
unit writes a
{ invariant(!a) and
sa_sz(!a) = sa_sz(old(!a)) and
model(!a, i) = v and
forall j:int. j <> i -> model(!a, j) = model(old(!a), j) }
*)
let set a i v =
{ 0 <= i < sa_sz(!a) and invariant(!a) }
let val = sa_val !a in
let idx = sa_idx !a in
let back = sa_back !a in
let sz= sa_sz !a in
let n = sa_n !a in
let val = A.store val i v in
if test a i then
a := (val, idx, back, sz, n)
else begin
assert { n < sz };
let idx = A.store idx i n in
let back = A.store back n i in
a := (val, idx, back, sz, n+1)
end
{ invariant(!a) and
sa_sz(!a) = sa_sz(old(!a)) and
model(!a, i) = v and
forall j:int. j <> i -> model(!a, j) = model(old(!a), j) }
let harness () =
let a = create 10 in
let b = create 20 in
let get_a_5 = get a 5 in assert { get_a_5 = default };
let get_b_7 = get b 7 in assert { get_b_7 = default };
set a 5 c1;
set b 7 c2;
let get_a_5 = get a 5 in assert { get_a_5 = c1 };
let get_b_7 = get b 7 in assert { get_b_7 = c2 };
let get_a_0 = get a 0 in assert { get_a_0 = default };
let get_b_0 = get b 0 in assert { get_b_0 = default };
()
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_sparse_array"
End:
*)
......@@ -59,12 +59,10 @@ let rec report fmt = function
Pgm_typing.report fmt e
| Denv.Error e ->
Denv.report fmt e
(*
| Ty.TypeMismatch (ty1, ty2) as e ->
eprintf "@[type mismatch: %a, %a@]@."
Pretty.print_ty ty1 Pretty.print_ty ty2;
raise e
*)
| e ->
raise e
......
......@@ -266,7 +266,7 @@ and unref_term env r v t = match t.t_node with
t_map (unref_term env r v) (unref env r v) t
(* quantify over all references in ef *)
let quantify env ef f =
let quantify ?(all=false) env ef f =
(* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
let quantify1 r f =
let ty = unref_ty env (E.type_of_reference r) in
......@@ -274,7 +274,8 @@ let quantify env ef f =
let f = unref env r v f in
wp_forall [v] [] f
in
let s = E.Sref.union ef.E.reads ef.E.writes in
let s = ef.E.writes in
let s = if all then E.Sref.union ef.E.reads s else s in
E.Sref.fold quantify1 s f
let abstract_wp env ef (q',ql') (q,ql) =
......@@ -516,7 +517,7 @@ and wp_desc env e q = match e.expr_desc with
and wp_triple env (p, e, q) =
let f = wp_expr env e q in
let f = wp_implies p f in
quantify env e.expr_effect f
quantify ~all:true env e.expr_effect f
let wp env e =
wp_expr env e (default_post e.expr_type e.expr_effect)
......
......@@ -179,6 +179,16 @@ let add_type (state, task) ts csl =
let ax = f_forall vl [[Term hd]] (f_equ hd t) in
add_decl tsk (create_prop_decl Paxiom pr ax)
in
let mt_add_single tsk cs t =
let id = mt_ls.ls_name.id_string ^ "_" ^ cs.ls_name.id_string in
let pr = create_prsymbol (id_derive id cs.ls_name) in
let vs = create_vsymbol (id_fresh "u") (of_option cs.ls_value) in
let hd = t_app mt_ls (t_var vs :: mt_tl) mt_ty in
let vl = List.rev_append mt_vl [vs] in
let ax = f_forall vl [[Term hd]] (f_equ hd t) in
add_decl tsk (create_prop_decl Paxiom pr ax)
in
let mt_add = if List.length csl = 1 then mt_add_single else mt_add in
let task = List.fold_left2 mt_add task csl mt_tl in
(* declare and define the projection functions *)
let pj_add (m,tsk) cs =
......
......@@ -47,16 +47,19 @@ theory ArrayKey
end
theory ArrayKeyLength
theory ArrayLength
type key
clone export ArrayKey with type key = key
clone export ArrayKey with type key = int
logic length('a t) : int
logic const_length('a, int) : 'a t
axiom Length_const :
forall a : 'a. forall n : int. length(const_length(a, n)) = n
axiom Length_store :
forall a : 'a t. forall k : key. forall v : 'a.
forall a : 'a t. forall k : int. forall v : 'a.
length(store(a, k, v)) = length(a)
end
......
......@@ -35,11 +35,6 @@ theory Prelude
end
theory Array
clone array.ArrayKeyLength with type key = int
end
(*
Local Variables:
......
Supports Markdown
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