Skip to content
GitLab
Commit 64ee8990 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

NumOf libraries look nicer with arrows instead of HO.pred

parent 0171d24a
Expand all Hide whitespace changes
Inline Side-by-side
examples/counting_sort/why3session.xml
View file @ 64ee8990
This diff is collapsed.
examples/inverse_in_place/why3session.xml
View file @ 64ee8990
......@@ -5,36 +5,35 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="6" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="3" name="Z3" version="3.2" timelimit="5" memlimit="4000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<file name="../inverse_in_place.mlw" expanded="true">
<theory name="InverseInPlace" sum="fafff34e116537414a710874d3420b0f" expanded="true">
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<file name="../inverse_in_place.mlw">
<theory name="InverseInPlace" sum="fafff34e116537414a710874d3420b0f">
<goal name="is_permutation_inverse">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place" expl="VC for inverse_in_place" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter inverse_in_place" expl="VC for inverse_in_place">
<transf name="split_goal_wp">
<goal name="WP_parameter inverse_in_place.1" expl="1. postcondition">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.2" expl="2. postcondition">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.3" expl="3. loop invariant init">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.4" expl="4. type invariant">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.5" expl="5. index in array bounds">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.6" expl="6. index in array bounds">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.7" expl="7. index in array bounds">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8" expl="8. loop invariant init">
<transf name="split_goal_wp">
......@@ -42,16 +41,16 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8.2" expl="2.">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="25"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8.3" expl="3.">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8.4" expl="4.">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8.5" expl="5.">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8.6" expl="6.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.03"/></proof>
......@@ -60,10 +59,10 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8.8" expl="8.">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.8.9" expl="9.">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
</transf>
</goal>
......@@ -71,24 +70,23 @@
<proof prover="0" memlimit="1000"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.10" expl="10. loop invariant init">
<proof prover="0" timelimit="5"><result status="valid" time="0.71"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="4.98"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.92"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.11" expl="11. type invariant">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.12" expl="12. index in array bounds">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.13" expl="13. index in array bounds">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.14" expl="14. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="3.82"/></proof>
<proof prover="4"><result status="valid" time="6.30"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.15" expl="15. loop invariant preservation">
<proof prover="0" memlimit="1000"><result status="valid" time="0.43"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.16" expl="16. loop invariant preservation">
<transf name="introduce_premises">
......@@ -97,10 +95,10 @@
<goal name="WP_parameter inverse_in_place.16.1.1" expl="1. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter inverse_in_place.16.1.1.1" expl="1.">
<proof prover="0" memlimit="1000"><result status="valid" time="1.38"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="2.34"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.16.1.1.2" expl="2.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.74"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="1.23"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.16.1.1.3" expl="3.">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -109,16 +107,16 @@
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.16.1.1.5" expl="5.">
<proof prover="4"><result status="valid" time="0.21"/></proof>
<proof prover="3"><result status="valid" time="0.21" steps="75"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.16.1.1.6" expl="6.">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.16.1.1.7" expl="7.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.96"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="1.64"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.16.1.1.8" expl="8.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.98"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="1.64"/></proof>
</goal>
</transf>
</goal>
......@@ -126,20 +124,20 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter inverse_in_place.17" expl="17. loop variant decrease" expanded="true">
<proof prover="1"><result status="valid" time="0.25"/></proof>
<goal name="WP_parameter inverse_in_place.17" expl="17. loop variant decrease">
<proof prover="1"><result status="valid" time="0.47"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.18" expl="18. assertion">
<proof prover="2"><result status="valid" time="0.80"/></proof>
<proof prover="2"><result status="valid" time="0.99"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.19" expl="19. assertion">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.20" expl="20. type invariant">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.21" expl="21. index in array bounds">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22" expl="22. loop invariant preservation">
<transf name="introduce_premises">
......@@ -148,30 +146,30 @@
<goal name="WP_parameter inverse_in_place.22.1.1" expl="1. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter inverse_in_place.22.1.1.1" expl="1.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.73"/></proof>
<proof prover="4"><result status="valid" time="2.70"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="0.95"/></proof>
<proof prover="3"><result status="valid" time="3.27" steps="110"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22.1.1.2" expl="2.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.88"/></proof>
<proof prover="4"><result status="valid" time="3.31"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="1.35"/></proof>
<proof prover="3"><result status="valid" time="4.53" steps="118"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22.1.1.3" expl="3.">
<proof prover="4"><result status="valid" time="2.03"/></proof>
<proof prover="3"><result status="valid" time="3.22" steps="73"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22.1.1.4" expl="4.">
<proof prover="5"><result status="valid" time="0.13"/></proof>
<proof prover="4"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22.1.1.5" expl="5.">
<proof prover="4"><result status="valid" time="0.37"/></proof>
<proof prover="3"><result status="valid" time="0.37" steps="113"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22.1.1.6" expl="6.">
<proof prover="5"><result status="valid" time="0.65"/></proof>
<proof prover="4"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22.1.1.7" expl="7.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.22.1.1.8" expl="8.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.61"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="0.86"/></proof>
</goal>
</transf>
</goal>
......@@ -180,10 +178,10 @@
</transf>
</goal>
<goal name="WP_parameter inverse_in_place.23" expl="23. assertion">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.24" expl="24. index in array bounds">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.25" expl="25. loop invariant preservation">
<transf name="introduce_premises">
......@@ -192,24 +190,24 @@
<goal name="WP_parameter inverse_in_place.25.1.1" expl="1. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter inverse_in_place.25.1.1.1" expl="1.">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="33"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.25.1.1.2" expl="2.">
<proof prover="4"><result status="valid" time="0.18"/></proof>
<proof prover="3"><result status="valid" time="0.18" steps="40"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.25.1.1.3" expl="3.">
<proof prover="5"><result status="valid" time="0.13"/></proof>
<proof prover="4"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.25.1.1.4" expl="4.">
<proof prover="5"><result status="valid" time="0.14"/></proof>
<proof prover="4"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.25.1.1.5" expl="5.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.15"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="36"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.25.1.1.6" expl="6.">
<proof prover="5"><result status="valid" time="0.24"/></proof>
<proof prover="4"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.25.1.1.7" expl="7.">
<proof prover="0" memlimit="1000"><result status="valid" time="0.54"/></proof>
......@@ -224,23 +222,23 @@
</transf>
</goal>
<goal name="WP_parameter inverse_in_place.26" expl="26. type invariant">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.27" expl="27. postcondition">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.28" expl="28. postcondition">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Harness" sum="897832384a9c012d857e3fb3a3f87d8e">
<goal name="WP_parameter test1" expl="VC for test1">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
<goal name="WP_parameter test2" expl="VC for test2">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
</theory>
</file>
......
modules/array.mlw
View file @ 64ee8990
......@@ -262,11 +262,12 @@ end
module NumOf
use import Array
use HighOrd as HO
use HighOrd
use import Bool
use int.NumOf as N
(** the number of a[i] such that [l <= i < u] and [pr i a[i]] *)
function numof (pr: HO.func int (HO.pred 'a)) (a: array 'a) (l u: int) : int =
function numof (pr: int -> 'a -> bool) (a: array 'a) (l u: int) : int =
N.numof (\ i. pr i a[i]) l u
end
......
theories/int.why
View file @ 64ee8990
......@@ -255,67 +255,68 @@ end
theory NumOf
use import Int
use HighOrd as HO
use HighOrd
use import Bool
function numof (p: HO.pred int) (a b: int) : int
function numof (p: int -> bool) (a b: int) : int
(** number of [n] such that [a <= n < b] and [p n] *)
axiom Numof_empty :
forall p: HO.pred int, a b: int.
forall p: int -> bool, a b: int.
b <= a -> numof p a b = 0
axiom Numof_right_no_add :
forall p : HO.pred int, a b : int.
forall p : int -> bool, a b : int.
a < b -> not (p (b-1)) -> numof p a b = numof p a (b-1)
axiom Numof_right_add :
forall p : HO.pred int, a b : int.
forall p : int -> bool, a b : int.
a < b -> p (b-1) -> numof p a b = 1 + numof p a (b-1)
lemma Numof_bounds :
forall p : HO.pred int, a b : int. a < b -> 0 <= numof p a b <= b - a
forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a
(* direct when a>=b, by induction on b when a <= b *)
lemma Numof_append :
forall p : HO.pred int, a b c : int.
forall p : int -> bool, a b c : int.
a <= b <= c -> numof p a c = numof p a b + numof p b c
(* by induction on c *)
lemma Numof_left_no_add :
forall p : HO.pred int, a b : int.
forall p : int -> bool, a b : int.
a < b -> not p a -> numof p a b = numof p (a+1) b
(* by Numof_append *)
lemma Numof_left_add :
forall p : HO.pred int, a b : int.
forall p : int -> bool, a b : int.
a < b -> p a -> numof p a b = 1 + numof p (a+1) b
(* by Numof_append *)
lemma Empty :
forall p : HO.pred int, a b : int.
forall p : int -> bool, a b : int.
(forall n : int. a <= n < b -> not p n) -> numof p a b = 0
(* by induction on b *)
lemma Full :
forall p : HO.pred int, a b : int. a <= b ->
forall p : int -> bool, a b : int. a <= b ->
(forall n : int. a <= n < b -> p n) -> numof p a b = b - a
(* by induction on b *)
lemma numof_increasing:
forall p : HO.pred int, i j k : int.
forall p : int -> bool, i j k : int.
i <= j <= k -> numof p i j <= numof p i k
(* by Numof_append and Numof_non_negative *)
lemma numof_strictly_increasing:
forall p: HO.pred int, i j k l: int.
forall p: int -> bool, i j k l: int.
i <= j <= k < l -> p k -> numof p i j < numof p i l
(* by Numof_append and numof_increasing *)
lemma numof_change_any:
forall p1 p2: HO.pred int, a b: int.
forall p1 p2: int -> bool, a b: int.
(forall j: int. a <= j < b -> p1 j -> p2 j) ->
numof p2 a b >= numof p1 a b
lemma numof_change_some:
forall p1 p2: HO.pred int, a b i: int. a <= i < b ->
forall p1 p2: int -> bool, a b i: int. a <= i < b ->
(forall j: int. a <= j < b -> p1 j -> p2 j) ->
not (p1 i) -> p2 i ->
numof p2 a b > numof p1 a b
......
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