simplified specifications involving theory NumOf

parent dcb6c555
......@@ -31,15 +31,15 @@ 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 = (M.map int int, int)
type param = (array int, int)
predicate eq (p: param) (i: int) = let (a,v) = p in M.get a i = v
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.elts, v) i j
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 M.get a i < v
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.elts, v) i j
function numlt (a: array int) (v i j : int) : int = Nlt.num_of (a, v) i j
(* an ovious lemma relates numeq and numlt *)
lemma eqlt:
......
......@@ -3,32 +3,16 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Definition unit := unit.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
......@@ -39,188 +23,192 @@ 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)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| (mk_array _ elts1) => elts1
(* Why3 assumption *)
Definition elts (a:Type)(v:(array a)): (map Z a) :=
match v with
| (mk_array x x1) => x1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| (mk_array length1 _) => length1
(* Why3 assumption *)
Definition length (a:Type)(v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
Implicit Arguments length.
(* Why3 assumption *)
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
(* Why3 assumption *)
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
end.
(mk_array (length a1) (set (elts a1) i v)).
Implicit Arguments set1.
(* Why3 assumption *)
Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z),
(((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a
(((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (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.
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 <= (get1 a i))%Z /\ ((get1 a i) < k)%Z).
(i < (length a))%Z) -> ((0%Z <= (get1 a i))%Z /\ ((get1 a i) < k)%Z).
Definition param := ((map Z Z)* Z)%type.
(* Why3 assumption *)
Definition param := ((array Z)* Z)%type.
Definition eq(p:((map Z Z)* Z)%type) (i:Z): Prop :=
(* Why3 assumption *)
Definition eq(p:((array Z)* Z)%type) (i:Z): Prop :=
match p with
| (a, v) => ((get a i) = v)
| (a, v) => ((get1 a i) = v)
end.
Parameter num_of: ((map Z Z)* Z)%type -> Z -> Z -> Z.
Parameter num_of: ((array Z)* Z)%type -> Z -> Z -> Z.
Axiom Num_of_empty : forall (p:((map Z Z)* Z)%type) (a:Z) (b: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:((map Z 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
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:((map Z 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
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:((map Z Z)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((0%Z <= (num_of p a b))%Z /\ ((num_of p a
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:((map Z Z)* Z)%type) (a:Z) (b:Z) (c: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:((map Z 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_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:((map Z 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
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:((map Z 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 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:((map Z 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
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:((map Z Z)* Z)%type) (i:Z) (j:Z) (k1: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:((map Z 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_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:((map Z Z)* Z)%type) (p2:((map Z Z)*
Z)%type) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((eq p1
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:((map Z Z)* Z)%type) (p2:((map Z 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))).
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))).
Definition numeq(a:(array Z)) (v:Z) (i:Z) (j:Z): Z := (num_of ((elts a), v) i
j).
(* Why3 assumption *)
Definition numeq(a:(array Z)) (v:Z) (i:Z) (j:Z): Z := (num_of (a, v) i j).
Definition lt(p:((map Z Z)* Z)%type) (i:Z): Prop :=
(* Why3 assumption *)
Definition lt(p:((array Z)* Z)%type) (i:Z): Prop :=
match p with
| (a, v) => ((get a i) < v)%Z
| (a, v) => ((get1 a i) < v)%Z
end.
Parameter num_of1: ((map Z Z)* Z)%type -> Z -> Z -> Z.
Parameter num_of1: ((array Z)* Z)%type -> Z -> Z -> Z.
Axiom Num_of_empty1 : forall (p:((map Z Z)* Z)%type) (a:Z) (b: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:((map Z 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
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:((map Z 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
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:((map Z Z)* Z)%type) (a:Z) (b:Z),
(a < b)%Z -> ((0%Z <= (num_of1 p a b))%Z /\ ((num_of1 p a
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:((map Z Z)* Z)%type) (a:Z) (b:Z) (c: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:((map Z 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
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:((map Z 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
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:((map Z 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 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:((map Z 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
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:((map Z Z)* Z)%type) (i:Z) (j:Z) (k1: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:((map Z 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_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:((map Z Z)* Z)%type) (p2:((map Z Z)*
Z)%type) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((lt p1
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:((map Z Z)* Z)%type) (p2:((map Z 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))).
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))).
Definition numlt(a:(array Z)) (v:Z) (i:Z) (j:Z): Z := (num_of1 ((elts a), v)
i j).
(* Why3 assumption *)
Definition numlt(a:(array Z)) (v:Z) (i:Z) (j:Z): Z := (num_of1 (a, v) i j).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* 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
((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)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros (n,m); simpl.
......@@ -242,11 +230,11 @@ rewrite Num_of_empty1; try omega.
rewrite Num_of_empty1; try omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
omega.
unfold get1; simpl; omega.
omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
intro; omega.
unfold get1; simpl; intro; omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
assumption.
......@@ -264,14 +252,14 @@ rewrite Num_of_empty1; try omega.
rewrite Num_of_empty1; try omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
omega.
unfold get1; 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.
intro; omega.
unfold get1; simpl; intro; omega.
rewrite Num_of_right_no_add1; try omega.
rewrite Num_of_right_no_add; try omega.
......@@ -284,15 +272,14 @@ rewrite Num_of_empty1; try omega.
rewrite Num_of_empty1; try omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
omega.
unfold get1; simpl; omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
omega.
unfold get1; simpl; omega.
red; simpl.
replace (Zsucc x - 1)%Z with x by omega.
omega.
unfold get1; simpl; omega.
Qed.
(* DO NOT EDIT BELOW *)
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -11,20 +11,20 @@ module Muller
use import module ref.Refint
use import module array.Array
type param = M.map int int
predicate pr (a: param) (n: int) = M.([]) a n <> 0
type param = array int
predicate pr (a: param) (n: int) = a[n] <> 0
clone import int.NumOfParam with type param = param, predicate pr = pr
let compact (a: array int) =
let count = ref 0 in
for i = 0 to length a - 1 do
invariant { 0 <= !count = num_of a.elts 0 i <= i}
invariant { 0 <= !count = num_of 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.elts 0 i <= i }
invariant { 0 <= !count = num_of a 0 i <= i }
if a[i] <> 0 then begin u[!count] <- a[i]; incr count end
done
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/jc/why3/share/why3session.dtd">
<why3session
name="programs/muller/why3session.xml" shape_version="2">
name="examples/programs/muller/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -17,22 +17,22 @@
<file
name="../muller.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="Muller"
locfile="programs/muller/../muller.mlw"
locfile="examples/programs/muller/../muller.mlw"
loclnum="8" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
<goal
name="WP_parameter compact"
locfile="programs/muller/../muller.mlw"
locfile="examples/programs/muller/../muller.mlw"
loclnum="18" loccnumb="6" loccnume="13"
expl="parameter compact"
sum="5b08aceebf544cb7cffdb12f1201eda0"
sum="9378f6b0c5f238005a17bf89d88f68b2"
proved="true"
expanded="true"
shape="iainfix =agetV1V6c0Nainfix &lt;=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix &lt;=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix &lt;V5V2Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix &lt;=c0V5Iainfix &lt;=V6ainfix -V0c1Aainfix &lt;=c0V6FFAainfix &lt;=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix &lt;=c0V3Iainfix &lt;=c0ainfix -V0c1Iainfix =V3c0FAainfix &gt;=V2c0Iainfix &lt;=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2Aiainfix =agetV1V9c0Nainfix &lt;=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V10anum_ofV1c0ainfix +V9c1Aainfix &lt;=c0V10Iainfix =V10ainfix +V2c1Fainfix &lt;=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V2anum_ofV1c0ainfix +V9c1Aainfix &lt;=c0V2Aainfix &lt;V9V0Aainfix &lt;=c0V9Iainfix &lt;=anum_ofV1c0V9V9Aainfix =V2anum_ofV1c0V9Aainfix &lt;=c0V2Iainfix &lt;=V9ainfix -V0c1Aainfix &lt;=c0V9FFAainfix &lt;=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Aiainfix =agetV1V14c0Nainfix &lt;=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V16anum_ofV1c0ainfix +V14c1Aainfix &lt;=c0V16Iainfix =V16ainfix +V13c1FIainfix =V15asetV12V13agetV1V14FAainfix &lt;V13c0Aainfix &lt;=c0V13Aainfix &lt;V14V0Aainfix &lt;=c0V14ainfix &lt;=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V13anum_ofV1c0ainfix +V14c1Aainfix &lt;=c0V13Aainfix &lt;V14V0Aainfix &lt;=c0V14Iainfix &lt;=anum_ofV1c0V14V14Aainfix =V13anum_ofV1c0V14Aainfix &lt;=c0V13Iainfix &lt;=V14ainfix -V0c1Aainfix &lt;=c0V14FFAainfix &lt;=anum_ofV1c0c0c0Aainfix =V11anum_ofV1c0c0Aainfix &lt;=c0V11Iainfix &lt;=c0ainfix -V0c1Iainfix =V11c0FAainfix &gt;=c0c0Iainfix &gt;c0ainfix -V0c1FF">
shape="iainfix =agetV1V7c0Nainfix &lt;=anum_ofV2c0ainfix +V7c1ainfix +V7c1Aainfix =V9anum_ofV2c0ainfix +V7c1Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1FIainfix =V8asetV5V6agetV1V7FAainfix &lt;V6V3Aainfix &lt;=c0V6Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;=anum_ofV2c0ainfix +V7c1ainfix +V7c1Aainfix =V6anum_ofV2c0ainfix +V7c1Aainfix &lt;=c0V6Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix &lt;=anum_ofV2c0V7V7Aainfix =V6anum_ofV2c0V7Aainfix &lt;=c0V6Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=c0V7FFAainfix &lt;=anum_ofV2c0c0c0Aainfix =V4anum_ofV2c0c0Aainfix &lt;=c0V4Iainfix &lt;=c0ainfix -V0c1Iainfix =V4c0FAainfix &gt;=V3c0Iainfix &lt;=anum_ofV2c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V3anum_ofV2c0ainfix +ainfix -V0c1c1Aainfix &lt;=c0V3Aiainfix =agetV1V10c0Nainfix &lt;=anum_ofV2c0ainfix +V10c1ainfix +V10c1Aainfix =V11anum_ofV2c0ainfix +V10c1Aainfix &lt;=c0V11Iainfix =V11ainfix +V3c1Fainfix &lt;=anum_ofV2c0ainfix +V10c1ainfix +V10c1Aainfix =V3anum_ofV2c0ainfix +V10c1Aainfix &lt;=c0V3Aainfix &lt;V10V0Aainfix &lt;=c0V10Iainfix &lt;=anum_ofV2c0V10V10Aainfix =V3anum_ofV2c0V10Aainfix &lt;=c0V3Iainfix &lt;=V10ainfix -V0c1Aainfix &lt;=c0V10FFAainfix &lt;=anum_ofV2c0c0c0Aainfix =c0anum_ofV2c0c0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Aiainfix =agetV1V15c0Nainfix &lt;=anum_ofV2c0ainfix +V15c1ainfix +V15c1Aainfix =V17anum_ofV2c0ainfix +V15c1Aainfix &lt;=c0V17Iainfix =V17ainfix +V14c1FIainfix =V16asetV13V14agetV1V15FAainfix &lt;V14c0Aainfix &lt;=c0V14Aainfix &lt;V15V0Aainfix &lt;=c0V15ainfix &lt;=anum_ofV2c0ainfix +V15c1ainfix +V15c1Aainfix =V14anum_ofV2c0ainfix +V15c1Aainfix &lt;=c0V14Aainfix &lt;V15V0Aainfix &lt;=c0V15Iainfix &lt;=anum_ofV2c0V15V15Aainfix =V14anum_ofV2c0V15Aainfix &lt;=c0V14Iainfix &lt;=V15ainfix -V0c1Aainfix &lt;=c0V15FFAainfix &lt;=anum_ofV2c0c0c0Aainfix =V12anum_ofV2c0c0Aainfix &lt;=c0V12Iainfix &lt;=c0ainfix -V0c1Iainfix =V12c0FAainfix &gt;=c0c0Iainfix &gt;c0ainfix -V0c1Lamk arrayV0V1FF">
<label
name="expl:parameter compact"/>
<transf
......@@ -41,13 +41,13 @@
expanded="true">
<goal
name="WP_parameter compact.1"
locfile="programs/muller/../muller.mlw"
locfile="examples/programs/muller/../muller.mlw"
loclnum="18" loccnumb="6" loccnume="13"
expl="precondition"
sum="65ba5df6446fbea7d8e602fba9cec2bd"
sum="24e42b00ba4e7a2639b799de1fc5370c"
proved="true"
expanded="true"
shape="ainfix &gt;=c0c0Iainfix &gt;c0ainfix -V0c1FF">
expanded="false"
shape="ainfix &gt;=c0c0Iainfix &gt;c0ainfix -V0c1Lamk arrayV0V1FF">
<label
name="expl:parameter compact"/>
<proof
......@@ -64,7 +64,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -72,18 +72,18 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter compact.2"
locfile="programs/muller/../muller.mlw"
locfile="examples/programs/muller/../muller.mlw"
loclnum="18" loccnumb="6" loccnume="13"
expl="for loop initialization"
sum="d3fe4b0c66ea6cda8b7ddb7e74f65b97"
sum="59779a641745b5d3b97d1c44bd5c1af3"
proved="true"
expanded="true"
shape="ainfix &lt;=anum_ofV1c0c0c0Aainfix =V2anum_ofV1c0c0Aainfix &lt;=c0V2Iainfix &lt;=c0ainfix -V0c1Iainfix =V2c0FIainfix &gt;=c0c0Iainfix &gt;c0ainfix -V0c1FF">
expanded="false"
shape="ainfix &lt;=anum_ofV2c0c0c0Aainfix =V3anum_ofV2c0c0Aainfix &lt;=c0V3Iainfix &lt;=c0ainfix -V0c1Iainfix =V3c0FIainfix &gt;=c0c0Iainfix &gt;c0ainfix -V0c1Lamk arrayV0V1FF">
<label
name="expl:parameter compact"/>
<proof
......@@ -92,7 +92,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="1"
......@@ -100,7 +100,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -108,18 +108,18 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter compact.3"
locfile="programs/muller/../muller.mlw"
locfile="examples/programs/muller/../muller.mlw"
loclnum="18" loccnumb="6" loccnume="13"
expl="for loop preservation"
sum="2a2d84890eb37f67073aa784a2e8c6a1"