library int.NumOf now takes some higher-order predicate as argument

no more need for cloning
similar change in array.NumOf and array.NumOfEq
updated proofs
parent 189ef30c
* marks an incompatible change
library
* renamed library int.NumOfParam into int.NumOf; the predicate numof
now takes some higher-order predicate as argument (no more need
for cloning). Similar change in modules array.NumOf...
version 0.85, September 17, 2014
================================
......
......@@ -18,6 +18,7 @@
module Spec
use export int.Int
use int.NumOf as N
use export array.Array
use export array.IntArraySorted
......@@ -31,22 +32,20 @@ module Spec
(* we introduce two predicates:
- [numeq a v l u] is the number of values in a[l..u[ equal to v
- [numlt a v l u] is the number of values in a[l..u[ less than v *)
type param = (array int, int)
function numeq (a: array int) (v i j : int) : int =
N.numof (\ k. a[k] = v) i j
predicate eq (p: param) (i: int) = let (a,v) = p in a[i] = v
clone int.NumOfParam as Neq with type param = param, predicate pr = eq
function numeq (a: array int) (v i j : int) : int = Neq.num_of (a, v) i j
predicate lt (p: param) (i: int) = let (a,v) = p in a[i] < v
clone int.NumOfParam as Nlt with type param = param, predicate pr = lt
function numlt (a: array int) (v i j : int) : int = Nlt.num_of (a, v) i j
function numlt (a: array int) (v i j : int) : int =
N.numof (\ k. a[k] < v) i j
(* an ovious lemma relates numeq and numlt *)
lemma eqlt:
forall a: array int. k_values a ->
forall v: int. 0 <= v < k ->
forall l u: int. 0 <= l < u <= length a ->
numlt a v l u + numeq a v l u = numlt a (v+1) l u
let rec lemma eqlt (a: array int) (v: int) (l u: int)
requires { k_values a }
requires { 0 <= v < k }
requires { 0 <= l < u <= length a }
ensures { numlt a v l u + numeq a v l u = numlt a (v+1) l u }
variant { u - l }
= if l < u-1 then eqlt a v (l+1) u
(* permutation of two arrays is here conveniently defined using [numeq]
i.e. as the equality of the two multi-sets *)
......
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
(* Why3 assumption *)
Definition sorted_sub (a:(@map.Map.map Z _ Z _)) (l:Z) (u:Z): Prop :=
forall (i1:Z) (i2:Z), ((l <= i1)%Z /\ ((i1 <= i2)%Z /\ (i2 < u)%Z)) ->
((map.Map.get a i1) <= (map.Map.get a i2))%Z.
(* Why3 assumption *)
Definition sorted_sub1 (a:(@array Z _)) (l:Z) (u:Z): Prop := (sorted_sub
(elts a) l u).
(* Why3 assumption *)
Definition sorted (a:(@array Z _)): Prop := (sorted_sub (elts a) 0%Z
(length a)).
Parameter k: Z.
Axiom k_positive : (0%Z < k)%Z.
(* Why3 assumption *)
Definition k_values (a:(@array Z _)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < (length a))%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < k)%Z).
(* Why3 assumption *)
Definition param := ((@array Z _)* Z)%type.
(* Why3 assumption *)
Definition eq (p:((@array Z _)* Z)%type) (i:Z): Prop :=
match p with
| (a, v) => ((get a i) = v)
end.
Parameter num_of: ((@array Z _)* Z)%type -> Z -> Z -> Z.
Axiom Num_of_empty : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(b <= a)%Z -> ((num_of p a b) = 0%Z).
Axiom Num_of_right_no_add : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((~ (eq p (b - 1%Z)%Z)) -> ((num_of p a b) = (num_of p a
(b - 1%Z)%Z))).
Axiom Num_of_right_add : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((eq p (b - 1%Z)%Z) -> ((num_of p a b) = (1%Z + (num_of p a
(b - 1%Z)%Z))%Z)).
Axiom Num_of_bounds : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((0%Z <= (num_of p a b))%Z /\ ((num_of p a
b) <= (b - a)%Z)%Z).
Axiom Num_of_append : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z) (c:Z),
((a <= b)%Z /\ (b <= c)%Z) -> ((num_of p a c) = ((num_of p a b) + (num_of p
b c))%Z).
Axiom Num_of_left_no_add : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((~ (eq p a)) -> ((num_of p a b) = (num_of p (a + 1%Z)%Z b))).
Axiom Num_of_left_add : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((eq p a) -> ((num_of p a b) = (1%Z + (num_of p (a + 1%Z)%Z
b))%Z)).
Axiom Empty : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z), (forall (n:Z),
((a <= n)%Z /\ (n < b)%Z) -> ~ (eq p n)) -> ((num_of p a b) = 0%Z).
Axiom Full : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z), (a <= b)%Z ->
((forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> (eq p n)) -> ((num_of p a
b) = (b - a)%Z)).
Axiom num_of_increasing : forall (p:((@array Z _)* Z)%type) (i:Z) (j:Z)
(k1:Z), ((i <= j)%Z /\ (j <= k1)%Z) -> ((num_of p i j) <= (num_of p i
k1))%Z.
Axiom num_of_strictly_increasing : forall (p:((@array Z _)* Z)%type) (i:Z)
(j:Z) (k1:Z) (l:Z), ((i <= j)%Z /\ ((j <= k1)%Z /\ (k1 < l)%Z)) -> ((eq p
k1) -> ((num_of p i j) < (num_of p i l))%Z).
Axiom num_of_change_any : forall (p1:((@array Z _)* Z)%type) (p2:((@array
Z _)* Z)%type) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) ->
((eq p1 j) -> (eq p2 j))) -> ((num_of p1 a b) <= (num_of p2 a b))%Z.
Axiom num_of_change_some : forall (p1:((@array Z _)* Z)%type) (p2:((@array
Z _)* Z)%type) (a:Z) (b:Z) (i:Z), ((a <= i)%Z /\ (i < b)%Z) ->
((forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((eq p1 j) -> (eq p2 j))) ->
((~ (eq p1 i)) -> ((eq p2 i) -> ((num_of p1 a b) < (num_of p2 a b))%Z))).
(* Why3 assumption *)
Definition numeq (a:(@array Z _)) (v:Z) (i:Z) (j:Z): Z := (num_of (a, v) i
j).
(* Why3 assumption *)
Definition lt (p:((@array Z _)* Z)%type) (i:Z): Prop :=
match p with
| (a, v) => ((get a i) < v)%Z
end.
Parameter num_of1: ((@array Z _)* Z)%type -> Z -> Z -> Z.
Axiom Num_of_empty1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(b <= a)%Z -> ((num_of1 p a b) = 0%Z).
Axiom Num_of_right_no_add1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((~ (lt p (b - 1%Z)%Z)) -> ((num_of1 p a b) = (num_of1 p a
(b - 1%Z)%Z))).
Axiom Num_of_right_add1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((lt p (b - 1%Z)%Z) -> ((num_of1 p a b) = (1%Z + (num_of1 p a
(b - 1%Z)%Z))%Z)).
Axiom Num_of_bounds1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((0%Z <= (num_of1 p a b))%Z /\ ((num_of1 p a
b) <= (b - a)%Z)%Z).
Axiom Num_of_append1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z) (c:Z),
((a <= b)%Z /\ (b <= c)%Z) -> ((num_of1 p a c) = ((num_of1 p a
b) + (num_of1 p b c))%Z).
Axiom Num_of_left_no_add1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((~ (lt p a)) -> ((num_of1 p a b) = (num_of1 p (a + 1%Z)%Z
b))).
Axiom Num_of_left_add1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((lt p a) -> ((num_of1 p a b) = (1%Z + (num_of1 p (a + 1%Z)%Z
b))%Z)).
Axiom Empty1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z), (forall (n:Z),
((a <= n)%Z /\ (n < b)%Z) -> ~ (lt p n)) -> ((num_of1 p a b) = 0%Z).
Axiom Full1 : forall (p:((@array Z _)* Z)%type) (a:Z) (b:Z), (a <= b)%Z ->
((forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> (lt p n)) -> ((num_of1 p a
b) = (b - a)%Z)).
Axiom num_of_increasing1 : forall (p:((@array Z _)* Z)%type) (i:Z) (j:Z)
(k1:Z), ((i <= j)%Z /\ (j <= k1)%Z) -> ((num_of1 p i j) <= (num_of1 p i
k1))%Z.
Axiom num_of_strictly_increasing1 : forall (p:((@array Z _)* Z)%type) (i:Z)
(j:Z) (k1:Z) (l:Z), ((i <= j)%Z /\ ((j <= k1)%Z /\ (k1 < l)%Z)) -> ((lt p
k1) -> ((num_of1 p i j) < (num_of1 p i l))%Z).
Axiom num_of_change_any1 : forall (p1:((@array Z _)* Z)%type) (p2:((@array
Z _)* Z)%type) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) ->
((lt p1 j) -> (lt p2 j))) -> ((num_of1 p1 a b) <= (num_of1 p2 a b))%Z.
Axiom num_of_change_some1 : forall (p1:((@array Z _)* Z)%type) (p2:((@array
Z _)* Z)%type) (a:Z) (b:Z) (i:Z), ((a <= i)%Z /\ (i < b)%Z) ->
((forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((lt p1 j) -> (lt p2 j))) ->
((~ (lt p1 i)) -> ((lt p2 i) -> ((num_of1 p1 a b) < (num_of1 p2 a b))%Z))).
(* Why3 assumption *)
Definition numlt (a:(@array Z _)) (v:Z) (i:Z) (j:Z): Z := (num_of1 (a, v) i
j).
(* Why3 goal *)
Theorem eqlt : forall (a:(@array Z _)), (k_values a) -> forall (v:Z),
((0%Z <= v)%Z /\ (v < k)%Z) -> forall (l:Z) (u:Z), ((0%Z <= l)%Z /\
((l < u)%Z /\ (u <= (length a))%Z)) -> (((numlt a v l u) + (numeq a v l
u))%Z = (numlt a (v + 1%Z)%Z l u)).
(* Why3 intros a h1 v (h2,h3) l u (h4,(h5,h6)). *)
(* YOU MAY EDIT THE PROOF BELOW *)
intros (n,m); simpl.
intros ha v hv l u hu.
unfold numlt, numeq; simpl.
generalize hu; pattern u; apply natlike_ind; intuition.
red in ha. unfold get in ha. simpl in ha.
assert (case: (Map.get m x < v \/ Map.get m x = v \/ Map.get m x > v)%Z) by omega. destruct case.
rewrite Num_of_right_add1; try omega.
rewrite Num_of_right_no_add.
rewrite Num_of_right_add1 with (b:=(Zsucc x)); try omega.
assert (case: (l < x \/ x <= l)%Z) by omega. destruct case.
ring_simplify.
replace (x+1-1)%Z with x by omega.
generalize (H7 H10); intuition.
rewrite Num_of_empty; try omega.
rewrite Num_of_empty1; try omega.
rewrite Num_of_empty1; try omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
unfold get; simpl; omega.
omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
unfold get; simpl; omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
assumption.
destruct H5.
rewrite Num_of_right_no_add1; try omega.
rewrite Num_of_right_add.
rewrite Num_of_right_add1 with (b:=(Zsucc x)); try omega.
assert (case: (l < x \/ x <= l)%Z) by omega. destruct case.
ring_simplify.
replace (x+1-1)%Z with x by omega.
generalize (H7 H10); intuition.
rewrite Num_of_empty; try omega.
rewrite Num_of_empty1; try omega.
rewrite Num_of_empty1; try omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
unfold get; simpl; omega.
omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
assumption.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
unfold get; simpl; omega.
rewrite Num_of_right_no_add1; try omega.
rewrite Num_of_right_no_add; try omega.
rewrite Num_of_right_no_add1 with (b:=(Zsucc x)); try omega.
assert (case: (l < x \/ x <= l)%Z) by omega. destruct case.
replace (Zsucc x - 1)%Z with x by omega.
apply H7; omega.
rewrite Num_of_empty; try omega.
rewrite Num_of_empty1; try omega.
rewrite Num_of_empty1; try omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
unfold get; simpl; omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
unfold get; simpl; omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
unfold get; simpl; omega.
Qed.
This diff is collapsed.
......@@ -12,7 +12,7 @@ module SimplePrioriyQueue
type elt
function priority elt : int
clone import array.NumOfEq with type elt = elt
use import array.NumOfEq
type t = {
elems: array elt;
......
......@@ -18,18 +18,14 @@
module InverseInPlace
use import int.Int
use int.NumOf
use import ref.Ref
use import array.Array
function (~_) (x: int) : int = -x-1
type param = M.map int int
predicate pr (a: param) (n: int) = M.([]) a n >= 0
clone import int.NumOfParam with type param = param, predicate pr = pr
lemma num_of_decrease:
forall m: param, l r i v: int. l <= i < r ->
M.get m i >= 0 -> v < 0 -> num_of (M.set m i v) l r < num_of m l r
function numof (m: M.map int int) (l r: int) : int =
NumOf.numof (\ n. M.([]) m n >= 0) l r
predicate is_permutation (a: array int) =
forall i: int. 0 <= i < length a ->
......@@ -72,7 +68,7 @@ module InverseInPlace
(at a 'L)[~ !j] = !k /\ a[~ !j] < 0 /\ a[m] < 0 }
invariant { forall e: int. 0 <= e < m -> a[e] < 0 -> a[e] <> !j }
invariant { loopinvariant (at a 'L) a m (m-1) n }
variant { num_of a.elts 0 n }
variant { numof a.elts 0 n }
a[!k] <- !j;
j := ~ !k;
k := !i;
......
This diff is collapsed.
......@@ -50,24 +50,25 @@ module LinearProbing
(** number of dummy values in array [a] between [l] and [u] *)
namespace NumOfDummy
type param = array key
predicate pr (a: param) (i: int) = eq a[i] dummy
clone export int.NumOfParam with type param = param, predicate pr = pr
use int.NumOf
function numof (a: array key) (l u: int) : int =
NumOf.numof (\ i. eq a[i] dummy) l u
let rec lemma numof_eq (a1 a2: array key) (l u: int) : unit
requires { 0 <= l <= u <= length a1 = length a2 }
requires { forall i: int. l <= i < u -> eq a2[i] a1[i] }
ensures { num_of a2 l u = num_of a1 l u }
ensures { numof a2 l u = numof a1 l u }
variant { u-l }
= if l < u then numof_eq a1 a2 (l+1) u
let rec lemma dummy_const (a: array key) (n: int)
requires { 0 <= n } requires { forall i: int. 0 <= i < n -> a[i] = dummy }
variant { n } ensures { num_of a 0 n = n }
variant { n } ensures { numof a 0 n = n }
= if n > 0 then dummy_const a (n-1)
end
function numofd (a: array key) (l u: int) : int = NumOfDummy.num_of a l u
function numofd (a: array key) (l u: int) : int = NumOfDummy.numof a l u
let ghost numof_update (a1 a2: array key) (l i u: int)
requires { 0 <= l <= i < u <= Array.length a1 = Array.length a2 }
......
This diff is collapsed.
......@@ -25,14 +25,13 @@ module Mjrty
use import int.Int
use import ref.Refint
use import array.Array
use import array.NumOfEq
exception Not_found
exception Found
type candidate
clone import array.NumOfEq with type elt = candidate
let mjrty (a: array candidate) : candidate
requires { 1 <= length a }
ensures { 2 * numof a result 0 (length a) > length a }
......
......@@ -4,67 +4,68 @@
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="30" memlimit="0"/>
<prover id="2" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<file name="../mjrty.mlw" expanded="true">
<theory name="Mjrty" sum="153bf2ddb44270a26a1c8d84c6e62339" expanded="true">
<theory name="Mjrty" sum="bf4383d5f7abd71536c53f1e6f7cdfcc" expanded="true">
<goal name="WP_parameter mjrty" expl="VC for mjrty" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter mjrty.1" expl="1. index in array bounds" expanded="true">
<goal name="WP_parameter mjrty.1" expl="1. index in array bounds">
<proof prover="1" timelimit="5" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter mjrty.2" expl="2. exceptional postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter mjrty.2" expl="2. exceptional postcondition">
<proof prover="1" timelimit="10"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mjrty.3" expl="3. loop invariant init" expanded="true">
<goal name="WP_parameter mjrty.3" expl="3. loop invariant init">
<proof prover="1" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mjrty.4" expl="4. loop invariant init" expanded="true">
<goal name="WP_parameter mjrty.4" expl="4. loop invariant init">
<proof prover="1" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mjrty.5" expl="5. loop invariant init" expanded="true">
<goal name="WP_parameter mjrty.5" expl="5. loop invariant init">
<proof prover="1" timelimit="10"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mjrty.6" expl="6. index in array bounds" expanded="true">
<goal name="WP_parameter mjrty.6" expl="6. index in array bounds">
<proof prover="1" timelimit="5" memlimit="1000"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter mjrty.7" expl="7. loop invariant preservation" expanded="true">
<proof prover="1" memlimit="1000"><result status="valid" time="0.18"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter mjrty.8" expl="8. loop invariant preservation" expanded="true">
<proof prover="1" memlimit="1000"><result status="valid" time="0.08"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="9.62"/></proof>
</goal>
<goal name="WP_parameter mjrty.9" expl="9. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.14"/></proof>
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter mjrty.10" expl="10. index in array bounds" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter mjrty.11" expl="11. loop invariant preservation" expanded="true">
<proof prover="1" memlimit="1000"><result status="valid" time="0.05"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.94"/></proof>
</goal>
<goal name="WP_parameter mjrty.12" expl="12. loop invariant preservation" expanded="true">
<proof prover="1" memlimit="1000"><result status="valid" time="0.05"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter mjrty.13" expl="13. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.40"/></proof>
<proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter mjrty.14" expl="14. loop invariant preservation" expanded="true">
<proof prover="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter mjrty.15" expl="15. loop invariant preservation" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="0.20"/></proof>
<proof prover="0" timelimit="30"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter mjrty.16" expl="16. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter mjrty.17" expl="17. exceptional postcondition" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.03"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter mjrty.18" expl="18. postcondition" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mjrty.19" expl="19. exceptional postcondition" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter mjrty.20" expl="20. loop invariant init" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.01"/></proof>
......@@ -73,16 +74,16 @@
<proof prover="1" timelimit="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mjrty.22" expl="22. postcondition" expanded="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="WP_parameter mjrty.23" expl="23. loop invariant preservation" expanded="true">
<proof prover="1" timelimit="5" memlimit="1000"><result status="valid" time="0.13"/></proof>
<proof prover="1" timelimit="5" memlimit="1000"><result status="valid" time="3.90"/></proof>
</goal>
<goal name="WP_parameter mjrty.24" expl="24. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter mjrty.25" expl="25. exceptional postcondition" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......
......@@ -10,21 +10,21 @@ module Muller
use import int.Int
use import ref.Refint
use import array.Array
use int.NumOf as N
type param = array int
predicate pr (a: param) (n: int) = a[n] <> 0
clone import int.NumOfParam with type param = param, predicate pr = pr
function numof (a: array int) (l u: int) : int =
N.numof (\ i. a[i] <> 0) l u
let compact (a: array int) =
let count = ref 0 in
for i = 0 to length a - 1 do
invariant { 0 <= !count = num_of a 0 i <= i}
invariant { 0 <= !count = numof a 0 i <= i}
if a[i] <> 0 then incr count
done;
let u = make !count 0 in
count := 0;
for i = 0 to length a - 1 do
invariant { 0 <= !count = num_of a 0 i <= i }
invariant { 0 <= !count = numof a 0 i <= i }
if a[i] <> 0 then begin u[!count] <- a[i]; incr count end
done
......
......@@ -2,86 +2,86 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<file name="../muller.mlw">
<theory name="Muller" sum="f81fe5d18d29157a26a0c948b9586043">
<goal name="WP_parameter compact" expl="VC for compact">
<transf name="split_goal_wp">
<goal name="WP_parameter compact.1" expl="1. array creation size">
<proof prover="0" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<file name="../muller.mlw" expanded="true">
<theory name="Muller" sum="b6f47ae25995fe503d061cd4c992c9d8" expanded="true">
<goal name="WP_parameter compact" expl="VC for compact" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter compact.1" expl="1. array creation size" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.2" expl="2. loop invariant init">
<proof prover="0" timelimit="10" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter compact.2" expl="2. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.3" expl="3. index in array bounds">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter compact.3" expl="3. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compact.4" expl="4. index in array bounds">
<goal name="WP_parameter compact.4" expl="4. index in array bounds" expanded="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter compact.5" expl="5. type invariant">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter compact.5" expl="5. type invariant" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter compact.6" expl="6. index in array bounds">
<proof prover="0" timelimit="10" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter compact.6" expl="6. index in array bounds" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compact.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter compact.8" expl="8. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter compact.7" expl="7. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter compact.9" expl="9. loop invariant init">
<proof prover="0" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter compact.8" expl="8. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter compact.9" expl="9. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.10" expl="10. index in array bounds">
<proof prover="0" timelimit="10" memlimit="0"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter compact.10" expl="10. index in array bounds" expanded="true">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.11" expl="11. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter compact.11" expl="11. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.91"/></proof>
</goal>
<goal name="WP_parameter compact.12" expl="12. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<goal name="WP_parameter compact.12" expl="12. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="WP_parameter compact.13" expl="13. array creation size">
<proof prover="0" timelimit="10" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter compact.13" expl="13. array creation size"