Skip to content

GitLab

why3
why3
Commit 94179377 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

programs: WP code refactored

parent 0fc6876e
Hide whitespace changes
Inline Side-by-side
Showing with 107 additions and 86 deletions
bench/bench
View file @ 94179377
......@@ -143,12 +143,13 @@ programs bench/programs/good
programs examples/programs
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== VC generation on good programs ==="
pgml_options=
programs bench/programs/good
programs examples/programs
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
examples/programs/decrease1/decrease1.mlw_Decrease1_decrease1_induction_2.v
View file @ 94179377
......@@ -18,34 +18,43 @@ Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition ref (a:Type) := a.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Parameter mixfix_lbrb: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Implicit Arguments mixfix_lbrb.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Parameter mixfix_lblsmnrb: forall (a:Type) (b:Type), (map a b) -> a -> b ->
(map a b).
Implicit Arguments set.
Implicit Arguments mixfix_lblsmnrb.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((mixfix_lbrb (mixfix_lblsmnrb m a1 b1) a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) ->
((mixfix_lbrb (mixfix_lblsmnrb m a1 b1) a2) = (mixfix_lbrb m a2)).
Parameter create_const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments create_const.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (create_const(b1):(map a b)) a1) = b1).
((mixfix_lbrb (const(b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
......@@ -63,17 +72,24 @@ Definition length (a:Type)(u:(array a)): Z :=
end.
Implicit Arguments length.
Definition mixfix_lbrb (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments mixfix_lbrb.
Definition mixfix_lbrb1 (a:Type)(a1:(array a)) (i:Z): a :=
(mixfix_lbrb (elts a1) i).
Implicit Arguments mixfix_lbrb1.
Definition mixfix_lblsmnrb1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (mixfix_lblsmnrb (elts a1) i v))
end.
Implicit Arguments mixfix_lblsmnrb1.
Definition decrease1(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < ((length a) - 1%Z)%Z)%Z) -> (((mixfix_lbrb a
i) - 1%Z)%Z <= (mixfix_lbrb a (i + 1%Z)%Z))%Z.
(i < ((length a) - 1%Z)%Z)%Z) -> (((mixfix_lbrb1 a
i) - 1%Z)%Z <= (mixfix_lbrb1 a (i + 1%Z)%Z))%Z.
Theorem decrease1_induction : forall (a:(array Z)), (decrease1 a) ->
forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\
(j < (length a))%Z) -> ((((mixfix_lbrb a
i) + i)%Z - j)%Z <= (mixfix_lbrb a j))%Z.
(j < (length a))%Z) -> ((((mixfix_lbrb1 a
i) + i)%Z - j)%Z <= (mixfix_lbrb1 a j))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
unfold decrease1.
intros a Ha i j Hij.
......@@ -86,11 +102,11 @@ destruct H4.
subst x.
ring_simplify.
omega.
apply Zle_trans with (mixfix_lbrb a (x-1) - 1)%Z.
apply Zle_trans with (mixfix_lbrb1 a (x-1) - 1)%Z.
assert (i <= x-1 < x)%Z by omega.
assert (0 <= i <= x-1 /\ x-1 < length a)%Z by omega.
generalize (H (x-1)%Z H8 H9); clear H; intuition.
apply Zle_trans with (mixfix_lbrb a (x-1+1))%Z.
apply Zle_trans with (mixfix_lbrb1 a (x-1+1))%Z.
apply (Ha (x-1)%Z); omega.
ring_simplify (x-1+1)%Z.
omega.
......
examples/programs/decrease1/why3session.xml
View file @ 94179377
......@@ -3,22 +3,22 @@
<why3session name="examples/programs/decrease1/why3session.xml">
<file name="../decrease1.mlw" verified="true" expanded="true">
<theory name="Decrease1" verified="true" expanded="true">
<goal name="decrease1_induction" sum="8319c3299f6c5b391aec5943ca151429" proved="true" expanded="true">
<goal name="decrease1_induction" sum="eb0923143934165c0f02dda5dd1d9064" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="decrease1.mlw_Decrease1_decrease1_induction_2.v" obsolete="false">
<result status="valid" time="0.75"/>
<result status="valid" time="0.74"/>
</proof>
</goal>
<goal name="WP_parameter search" expl="correctness of parameter search" sum="46e3d9215dcd11606cc49de64a5a327f" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search.1" expl="loop invariant init" sum="f5954e0aa354b70603e2561453b4ded0" proved="true" expanded="true">
<goal name="WP_parameter search" expl="correctness of parameter search" sum="5ecc8b47f440f11c94bcb33eb0c0f5da" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter search.1" expl="loop invariant init" sum="c3003e2b17bd7912bbde842b069e15bc" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter search.2" expl="precondition" sum="f0aee083a6eefd91f49d716bfaf3a741" proved="true" expanded="true">
<goal name="WP_parameter search.2" expl="precondition" sum="a9e24466223260e82e53917990341c5a" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......@@ -26,36 +26,44 @@
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search.3" expl="normal postcondition" sum="c09d1921f62c8a7957bab3179290a800" proved="true" expanded="true">
<goal name="WP_parameter search.3" expl="normal postcondition" sum="c463c5623e8270cf898748cd4fc200db" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search.4" expl="precondition" sum="fafef13cd1de3a63dcb73b0bead2cbe7" proved="true" expanded="true">
<goal name="WP_parameter search.4" expl="precondition" sum="c9ffe9627c38578519b5fb654bc2311b" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter search.5" expl="precondition" sum="60fccac213582dacf78a1595c1a07a68" proved="true" expanded="true">
<goal name="WP_parameter search.5" expl="precondition" sum="87f27d100b565712984fd9fda61cce4e" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter search.6" expl="loop invariant preservation" sum="726cc05d33c2e38e4510462e1e7605e2" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.35"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search.6" expl="loop invariant preservation" sum="f4703704714fb12b1cfc7e1f7033703a" proved="true" expanded="true">
<goal name="WP_parameter search.7" expl="loop variant decreases" sum="2b005062b036872b0521075f47993799" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search.7" expl="loop variant decreases" sum="fbefe9d12ef4966b8e4cd42008951924" proved="true" expanded="true">
<goal name="WP_parameter search.8" expl="loop invariant preservation" sum="8c2b5cf695743e9c3d5c78cda24518fe" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
......@@ -63,25 +71,17 @@
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search.8" expl="loop invariant preservation" sum="7c213b031c337fec29d0003aec1f4dc0" proved="true" expanded="true">
<goal name="WP_parameter search.9" expl="loop variant decreases" sum="6180bf4f47e0f340cb46853306f6bf48" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter search.9" expl="loop variant decreases" sum="c65a3f1470a58687f3ba32fd10a257dc" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search.10" expl="normal postcondition" sum="aed189de59d328d4a7873cf4ad31f1ee" proved="true" expanded="true">
<goal name="WP_parameter search.10" expl="normal postcondition" sum="df0f4238e9b7a001efd85670c5738437" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
......@@ -89,9 +89,9 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter search_rec" expl="correctness of parameter search_rec" sum="9fb29a60c6f5cf8d6b537c46b8c3ba87" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search_rec.1" expl="precondition" sum="e99d8b29c61d5561f42de7428f854f98" proved="true" expanded="true">
<goal name="WP_parameter search_rec" expl="correctness of parameter search_rec" sum="e89966a62cd9e50970addcdec10b6caa" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter search_rec.1" expl="precondition" sum="129dba47026aaf884be22c8cbc1d4a1a" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......@@ -99,31 +99,31 @@
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.2" expl="normal postcondition" sum="d0e9788d6a49388120275a1794f251ca" proved="true" expanded="true">
<goal name="WP_parameter search_rec.2" expl="normal postcondition" sum="c7add74865ef8eb3cc7e152b836f6394" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.3" expl="precondition" sum="81a8eda76bb9fc55426d0d2c779fb747" proved="true" expanded="true">
<goal name="WP_parameter search_rec.3" expl="precondition" sum="752cd932517186cc6711edbfdc9cdcc5" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.4" expl="precondition" sum="1aa5fc2b9d9f2274df86f567e8367758" proved="true" expanded="true">
<goal name="WP_parameter search_rec.4" expl="precondition" sum="70200655836e750408cd8a5996962583" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.5" expl="precondition" sum="df4ce06ace5afed63c8806a0409bc373" proved="true" expanded="true">
<goal name="WP_parameter search_rec.5" expl="precondition" sum="3c0ace1c9d0462dad22f9a3def392d80" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......@@ -131,12 +131,12 @@
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.6" expl="normal postcondition" sum="66a382fecdcc926c2651f0df8b934922" proved="true" expanded="true">
<goal name="WP_parameter search_rec.6" expl="normal postcondition" sum="5e4e50fa7d00a3e211e6c765447598ac" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.24"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.7" expl="precondition" sum="3cd087502acbddf93bedd2e7ae41368f" proved="true" expanded="true">
<goal name="WP_parameter search_rec.7" expl="precondition" sum="59fbd71468455b495415851791a881e4" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......@@ -144,15 +144,15 @@
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.8" expl="normal postcondition" sum="aa8066ccccfb75f3b09a443bfcc18824" proved="true" expanded="true">
<goal name="WP_parameter search_rec.8" expl="normal postcondition" sum="23b6323ce32882d20cbec4416c19c5fc" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter search_rec.9" expl="normal postcondition" sum="43a3bb410f2b3ac8d455124eb75c46bc" proved="true" expanded="true">
<goal name="WP_parameter search_rec.9" expl="normal postcondition" sum="a6ad2af03185d4f9110d519f3155f374" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......
src/programs/pgm_pretty.ml
View file @ 94179377
......@@ -23,10 +23,10 @@ let rec print_expr fmt e = match e.expr_desc with
| Eglobal { ps_kind = PSlogic } ->
assert false
| Efun (bl, t) ->
fprintf fmt "@[<hov 2>fun %a ->@ %a@]"
fprintf fmt "@[<hov 2>fun %a ->@ %a@]"
(print_list space print_pv) bl print_triple t
| Elet (v, e1, e2) ->
fprintf fmt "@[<hv 0>@[<hov 2>let %a/%a =@ %a in@]@ %a@]"
fprintf fmt "@[<hv 0>@[<hov 2>let %a/%a =@ %a in@]@ %a@]"
print_vs v.pv_effect print_vs v.pv_pure
print_expr e1 print_expr e2
......@@ -64,12 +64,12 @@ and print_triple fmt (p, e, q) =
fprintf fmt "@[<hv 0>%a@ %a@ %a@]" print_pre p print_expr e print_post q
and print_recfun fmt (v, bl, _, t) =
fprintf fmt "@[<hov 2>rec %a@ %a =@ %a@]"
fprintf fmt "@[<hov 2>rec %a@ %a =@ %a@]"
print_pv v (print_list space print_pv) bl print_triple t
and print_branch fmt (p, e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pattern p print_expr e
and print_pattern fmt p =
and print_pattern fmt p =
Pretty.print_pat fmt p.ppat_pat
src/programs/pgm_wp.ml
View file @ 94179377
......@@ -152,6 +152,22 @@ let find_constructor env ts =
| [ls] -> ls
| _ -> assert false
let wp_close rm ef f =
let sreg = ef.E.writes in
let sreg =
Spv.fold (fun pv s -> Sreg.union pv.pv_regions s)
ef.E.globals (Sreg.union ef.E.reads sreg)
in
(* all program variables involving these regions *)
let vars =
let add r s =
try Spv.union (Mreg.find r rm) s with Not_found -> assert false
in
Sreg.fold add sreg Spv.empty
in
let quantify_v v f = wp_forall v.pv_pure f in
Spv.fold quantify_v vars f
(* quantify over all references in ef
ef : effect
rm : region -> pvsymbol set
......@@ -174,15 +190,8 @@ let find_constructor env ts =
forall v'. f[v <- v']
*)
let quantify ?(all=false) env rm ef f =
let quantify env rm ef f =
let sreg = ef.E.writes in
let sreg =
if all then
Spv.fold (fun pv s -> Sreg.union pv.pv_regions s)
ef.E.globals (Sreg.union ef.E.reads sreg)
else
sreg
in
(* mreg: rho -> rho' *)
let mreg =
let add r m =
......@@ -217,7 +226,7 @@ let quantify ?(all=false) env rm ef f =
mreg, Mvs.add pv.pv_pure v' s, vv'
end else begin
eprintf "pv = %a@." print_pvsymbol pv;
assert false (*TODO*)
failwith "WP: update not yet implemented" (* assert false *)
end
| Ty.Tyvar _ ->
assert false
......@@ -567,7 +576,7 @@ and wp_triple env rm bl (p, e, q) =
in
let f = wp_expr env rm e q in
let f = wp_implies p f in
let f = quantify ~all:true env rm e.expr_effect f in
let f = wp_close rm e.expr_effect f in
wp_binders bl f
and wp_recfun env rm (_, bl, _var, t) =
......@@ -625,7 +634,7 @@ let decl uc = function
add_wp_decl ps f uc
| Pgm_ttree.Dletrec dl ->
let add_one uc (ps, def) =
let f = wp_recfun uc Mreg.empty def in
let f = wp_recfun uc !global_regions def in
Debug.dprintf debug "wp %s = %a@\n----------------@."
ps.ps_impure.ls_name.id_string Pretty.print_term f;
add_wp_decl ps f uc
......
tests/test-pgm-jcf.mlw
View file @ 94179377
......@@ -5,15 +5,10 @@ module M
parameter x : ref int
let bar () = {} x := 1 { !x = 1 }
parameter foo : y:int -> { y <> 0 } int { true }
let test_and_2 () = { !x > 0 } foo !x {}
let rec f2 () : unit = { } x := 1; f2 () { }
end
(***
module TestArray
......
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