cleaning up same_fringe and sparse_array

parent 1c47e80c
......@@ -7,7 +7,9 @@
module SameFringe
use import int.Int
use import list.List
use import list.Length
use import list.Append
(* binary trees with elements at the nodes *)
......@@ -36,7 +38,14 @@ module SameFringe
(* the enum of a tree [t], prepended to a given enum [e] *)
let rec enum t e =
logic leftlen (t: tree) : int = match t with
| Empty -> 0
| Node l _ _ -> 1 + leftlen l
end
lemma leftlen_nonneg: forall t: tree. leftlen t >= 0
let rec enum t e variant { leftlen t } =
{ }
match t with
| Empty -> e
......@@ -44,7 +53,7 @@ module SameFringe
end
{ enum_elements result = elements t ++ enum_elements e }
let rec eq_enum e1 e2 =
let rec eq_enum e1 e2 variant { length (enum_elements e1) } =
{ }
match e1, e2 with
| Done, Done ->
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter infix_plpl: forall (a:Type), (list a) -> (list a) -> (list a).
Implicit Arguments infix_plpl.
Axiom infix_plpl_def : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
match l1 with
| Nil => ((infix_plpl l1 l2) = l2)
| Cons x1 r1 => ((infix_plpl l1 l2) = (Cons x1 (infix_plpl r1 l2)))
end.
Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil:(list a))) = l).
Parameter length: forall (a:Type), (list a) -> Z.
Implicit Arguments length.
Axiom length_def : forall (a:Type), forall (l:(list a)),
match l with
| Nil => ((length l) = 0%Z)
| Cons _ r => ((length l) = (1%Z + (length r))%Z)
end.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil:(list a))).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
Parameter mem: forall (a:Type), a -> (list a) -> Prop.
Implicit Arguments mem.
Axiom mem_def : forall (a:Type), forall (x:a) (l:(list a)),
match l with
| Nil => ~ (mem x l)
| Cons y r => (mem x l) <-> ((x = y) \/ (mem x r))
end.
Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
Parameter elt : Type.
Inductive tree :=
| Empty : tree
| Node : tree -> elt -> tree -> tree .
Parameter elements: tree -> (list elt).
Axiom elements_def : forall (t:tree),
match t with
| Empty => ((elements t) = (Nil:(list elt)))
| Node l x r => ((elements t) = (infix_plpl (elements l) (Cons x
(elements r))))
end.
Inductive enum :=
| Done : enum
| Next : elt -> tree -> enum -> enum .
Parameter enum_elements: enum -> (list elt).
Axiom enum_elements_def : forall (e:enum),
match e with
| Done => ((enum_elements e) = (Nil:(list elt)))
| Next x r e1 => ((enum_elements e) = (Cons x (infix_plpl (elements r)
(enum_elements e1))))
end.
Parameter leftlen: tree -> Z.
Axiom leftlen_def : forall (t:tree),
match t with
| Empty => ((leftlen t) = 0%Z)
| Node l _ _ => ((leftlen t) = (1%Z + (leftlen l))%Z)
end.
Theorem leftlen_nonneg : forall (t:tree), (0%Z <= (leftlen t))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
induction t;
intuition.
rewrite (leftlen_def Empty).
omega.
rewrite (leftlen_def (Node t1 e t2)).
omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -3,19 +3,59 @@
<why3session name="examples/programs/same_fringe/why3session.xml">
<file name="../same_fringe.mlw" verified="true" expanded="true">
<theory name="SameFringe" verified="true" expanded="true">
<goal name="WP_enum" expl="correctness of enum" sum="a88e6bbf942db53576d5061640c13823" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.64"/>
<goal name="leftlen_nonneg" sum="9e80575f6e2af3d97ea15e644db5db14" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="same_fringe.mlw_SameFringe_leftlen_nonneg_1.v" obsolete="false">
<result status="valid" time="0.59"/>
</proof>
</goal>
<goal name="WP_eq_enum" expl="correctness of eq_enum" sum="11a451fdc4d6ebb10c4d89b5081d5aa9" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<goal name="WP_parameter enum" expl="correctness of parameter enum" sum="400dbb18200455814ca6e566343047e6" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.84"/>
</proof>
</goal>
<goal name="WP_same_fringe" expl="normal postcondition" sum="aab1ac13bc5135eb61f706e2989a61b0" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<goal name="WP_parameter eq_enum" expl="correctness of parameter eq_enum" sum="70b74c191411efdf762cca0c55ea9f7c" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.1" expl="correctness of parameter eq_enum" sum="8efd103daf9ddccb43746a8d352ad0e5" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.07"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.06"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.2" expl="correctness of parameter eq_enum" sum="55ffebc1aea30da2b2cadc0dd6637f0c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.3" expl="correctness of parameter eq_enum" sum="b53fbfedc75c5b5ec5ac70d08cf8b227" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.4" expl="correctness of parameter eq_enum" sum="6c0281f01c50610cb3cd19d653d1d708" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.5" expl="correctness of parameter eq_enum" sum="ccebd2695c718ca0752b3d797f508b10" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.6" expl="correctness of parameter eq_enum" sum="36c65fbebc64ad2a8e593310f4a5bc27" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter same_fringe" expl="normal postcondition" sum="84928bdc563afca8c3391397c48ceba3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
......@@ -47,7 +47,7 @@ back +-+-+-+-------------------+
else
default
logic invariant_ (a : sparse_array) =
logic sa_invariant (a : sparse_array) =
0 <= a.card <= length a <= maxlen and
A.length a.val = A.length a.idx = A.length a.back and
forall i : int.
......@@ -76,7 +76,7 @@ back +-+-+-+-------------------+
a[dirichlet n a i] = i)
lemma Inter6 :
forall a : sparse_array . invariant_ a ->
forall a : sparse_array . sa_invariant a ->
a.card = length a ->
permutation a.card a.back &&
forall i : int. 0 <= i < a.card ->
......@@ -87,17 +87,17 @@ back +-+-+-+-------------------+
let create sz =
{ 0 <= sz <= maxlen }
{| val = malloc sz; idx = malloc sz; back = malloc sz; card = 0 |}
{ invariant_ result and
{ sa_invariant result and
result.card = 0 and
length result = sz and forall i:int. model result i = default }
let test (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
{ 0 <= i < length a and sa_invariant a }
0 <= a.idx[i] && a.idx[i] < a.card && a.back[a.idx[i]] = i
{ result=True <-> is_elt a i }
let get (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
{ 0 <= i < length a and sa_invariant a }
if test a i then
(val a)[i]
else
......@@ -105,7 +105,7 @@ back +-+-+-+-------------------+
{ result = model a i }
let set (a: sparse_array) i v =
{ 0 <= i < length a and invariant_ a }
{ 0 <= i < length a and sa_invariant a }
a.val[i] <- v;
if not (test a i) then begin
assert { a.card < length a };
......@@ -113,7 +113,7 @@ back +-+-+-+-------------------+
a.back[a.card] <- i;
a.card <- a.card + 1
end
{ invariant_ a and
{ sa_invariant a and
model a i = v and
forall j:int. j <> i -> model a j = model (old a) j }
......
o bug in test-pgm-jcf: incr_fst
o bug in test-pgm-jcf: scope
o old(...) should not contain any local logical variable (let / match)
o freshness analysis
o no `old' in loop invariants
......@@ -12,6 +18,8 @@ o syntactic sugar for postcondition:
but also { a,b | ... }, etc.
o automatically add a label pre_f at entrance of each function f
and then replace (old t) by (at t pre_f)
(so that there is no more 'old' in the abstract syntax)
o use of old in loop invariant should be reported as an error (correctly)
......
......@@ -1407,17 +1407,9 @@ let mk_bool_constant loc gl ls =
let mk_false loc gl = mk_bool_constant loc gl (find_ls ~pure:true gl "False")
let mk_true loc gl = mk_bool_constant loc gl (find_ls ~pure:true gl "True")
(* types do not contain inner reference types *)
let rec check_type ?(noref=false) gl loc ty = match ty.ty_node with
| Ty.Tyapp (ts, tyl) when ts_equal ts ts_arrow ->
List.iter (check_type gl loc) tyl
| Ty.Tyapp (ts, _) when noref && is_mutable_ts ts ->
errorm ~loc "inner reference types are not allowed"
| Ty.Tyapp (_, tyl) ->
List.iter (check_type ~noref:true gl loc) tyl
| Ty.Tyvar _ ->
()
(* check that variables occurring in 'old' and 'at' are not local variables *)
let check_at_fmla f =
assert false (*TODO*)
(* Saturation of postconditions: a postcondition must be set for
any possibly raised exception *)
......@@ -1456,7 +1448,6 @@ let rec expr gl env e =
let ty = e.iexpr_type in
let loc = e.iexpr_loc in
let d, v, ef = expr_desc gl env loc ty e.iexpr_desc in
check_type gl loc ty; (* TODO: improve efficiency *)
{ expr_desc = d; expr_type = ty;
expr_type_v = v; expr_effect = ef; expr_loc = loc }
......
......@@ -16,11 +16,23 @@ module M
r := 0
{ !r = 0 }
logic fst (x: ('a, 'b)) : 'a = let (x1, _) = x in x1
(* BUG *)
let incr_fst (a: (ref int, int)) =
{} let (r,_) = a in r := !r + 1 { !(fst a) = (old !(fst a)) + 1 }
let test4 () =
let r = ref 0 in
let a = (r, 0) in
incr_fst a;
assert { !(fst a) = 1 }
(* BUG: x escapes its scope (in the postcondition) => should be an error *)
(* let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !x = 0 } *)
(* let scope (a: ref int) = let x = a in fun () -> {} x := 0 { !x = 0 } *)
let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !a = 0 }
let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } end
let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } 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