Commit a8c13660 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

update proof session

parent 54f0afbe
(* 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 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.
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.
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)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set 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)).
Parameter const: forall (b:Type) (a: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), ((get (const(
b1):(map a b)) a1) = b1).
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
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| (mk_array length1 _) => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
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.
Implicit Arguments set1.
Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
(u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
Implicit Arguments map_eq_sub.
Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
(j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
Implicit Arguments exchange.
Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
(j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
(u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
Implicit Arguments permut_sub.
Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z
a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\
(r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/
(u <= i)%Z) -> ((get a2 i) = (get a1 i)).
Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2
i) = (get a1 j)).
Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
(j:Z): Prop := (exchange (elts a1) (elts a2) i j).
Implicit Arguments exchange1.
Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
Implicit Arguments permut_sub1.
Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z
(length a1)).
Implicit Arguments permut.
Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a))
(i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) ->
(((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\
(j < (length a1))%Z) -> (permut a1 a2)))).
Axiom permut_sym1 : forall (a:Type), forall (a1:(array a)) (a2:(array a)),
(permut a1 a2) -> (permut a2 a1).
Axiom permut_trans1 : forall (a:Type), forall (a1:(array a)) (a2:(array a))
(a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)).
Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
Implicit Arguments array_eq_sub.
Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)).
Implicit Arguments array_eq.
Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u).
Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)), (array_eq a1 a2) -> (permut a1 a2).
Definition le(x:bool) (y:bool): Prop := (x = false) \/ (y = true).
Definition sorted(a:(array bool)): Prop := forall (i1:Z) (i2:Z),
(((0%Z <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < (length a))%Z) -> (le (get1 a
i1) (get1 a i2)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_two_way_sort : forall (a:Z), forall (a1:(map Z bool)),
let a2 := (mk_array a a1) in forall (j:Z), forall (i:Z), forall (a3:(map Z
bool)), ((0%Z <= i)%Z /\ ((j < a)%Z /\ ((permut a2 (mk_array a a3)) /\
((forall (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) -> ~ ((get a3 k) = true)) /\
forall (k:Z), ((j < k)%Z /\ (k < a)%Z) -> ((get a3 k) = true))))) ->
((i < j)%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> (((get a3 i) = true) ->
(((0%Z <= j)%Z /\ (j < a)%Z) -> ((~ ((get a3 j) = true)) ->
((((0%Z <= i)%Z /\ (i < a)%Z) /\ ((0%Z <= j)%Z /\ (j < a)%Z)) ->
forall (a4:(map Z bool)), (exchange a3 a4 i j) -> forall (i1:Z),
(i1 = (i + 1%Z)%Z) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2
(mk_array a a4)))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
apply permut_trans1 with (mk_array a a3); auto.
apply exchange_permut with i j; auto.
Qed.
(* DO NOT EDIT BELOW *)
(* 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 bool.Bool.
Require map.Map.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
(* 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 map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _
a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\
(((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\
(u <= (length a1))%Z) /\ (map_eq_sub (elts a1) (elts a2) l u))).
(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub
(elts a1) (elts a2) 0%Z (length a1)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\
(((0%Z <= i)%Z /\ (i < (length a1))%Z) /\ (((0%Z <= j)%Z /\
(j < (length a1))%Z) /\ (((get a1 i) = (get a2 j)) /\ (((get a1
j) = (get a2 i)) /\ forall (k:Z), ((0%Z <= k)%Z /\ (k < (length a1))%Z) ->
((~ (k = i)) -> ((~ (k = j)) -> ((get a1 k) = (get a2 k)))))))).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array
a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\
(((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\
(u <= (length a1))%Z) /\ (map.MapPermut.permut (elts a1) (elts a2) l u))).
(* Why3 assumption *)
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2)
0%Z l) /\ ((permut a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u
(length a1))).
(* Why3 assumption *)
Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\
(map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)).
Axiom permut_all_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)), (permut_all a1 a1).
Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1
a2 i j) -> (permut_all a1 a2).
Axiom permut_all_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (a2:(@array a a_WT)), (permut_all a1 a2) -> (permut_all a2 a1).
Axiom permut_all_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut_all a1 a2) ->
((permut_all a2 a3) -> (permut_all a1 a3)).
Axiom array_eq_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) ->
(permut_all a1 a2).
Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z)
(u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) ->
(((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))).
Axiom permut_sub_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub
a1 a2 l u) -> (permut_all a1 a2).
(* Why3 assumption *)
Definition le (x:bool) (y:bool): Prop := (x = false) \/ (y = true).
(* Why3 assumption *)
Definition sorted (a:(@array bool _)): Prop := forall (i1:Z) (i2:Z),
((0%Z <= i1)%Z /\ ((i1 <= i2)%Z /\ (i2 < (length a))%Z)) -> (le (get a i1)
(get a i2)).
(* Why3 goal *)
Theorem WP_parameter_two_way_sort : forall (a:Z) (a1:(@map.Map.map Z _
bool _)), let a2 := (mk_array a a1) in ((0%Z <= a)%Z -> forall (j:Z) (i:Z)
(a3:(@map.Map.map Z _ bool _)), let a4 := (mk_array a a3) in
(((0%Z <= i)%Z /\ ((j < a)%Z /\ ((permut_all a2 a4) /\ ((forall (k:Z),
((0%Z <= k)%Z /\ (k < i)%Z) -> ((map.Map.get a3 k) = false)) /\
forall (k:Z), ((j < k)%Z /\ (k < a)%Z) -> ((map.Map.get a3
k) = true))))) -> ((i < j)%Z -> (((0%Z <= a)%Z /\ ((0%Z <= i)%Z /\
(i < a)%Z)) -> (((map.Map.get a3 i) = true) -> (((0%Z <= j)%Z /\
(j < a)%Z) -> ((~ ((map.Map.get a3 j) = true)) -> ((((0%Z <= i)%Z /\
(i < a)%Z) /\ ((0%Z <= j)%Z /\ (j < a)%Z)) -> forall (a5:(@map.Map.map Z _
bool _)), let a6 := (mk_array a a5) in (((0%Z <= a)%Z /\ (exchange a4 a6 i
j)) -> forall (i1:Z), (i1 = (i + 1%Z)%Z) -> forall (j1:Z),
(j1 = (j - 1%Z)%Z) -> (permut_all a2 a6)))))))))).
(* Why3 intros a a1 a2 h1 j i a3 a4 (h2,(h3,(h4,(h5,h6)))) h7 (h8,(h9,h10))
h11 (h12,h13) h14 ((h15,h16),(h17,h18)) a5 a6 (h19,h20) i1 h21 j1
h22. *)
(* intros a a1 a2 h1 j i a3 (h2,(h3,(h4,(h5,h6)))) h7 (h8,(h9,h10)) h11
(h12,h13) h14 ((h15,h16),(h17,h18)) a4 (h19,h20) i1 h21 j1 h22. *)
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
apply permut_all_trans with (mk_array a a3); auto.
apply exchange_permut_all with i j; auto.
Qed.
......@@ -7,16 +7,12 @@
version="0.95.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.2"/>
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Coq"
version="8.4pl2"/>
<file
name="../vstte12_two_way_sort.mlw"
verified="true"
......@@ -32,7 +28,7 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="VC for two_way_sort"
sum="9a06e54f2891cbf51a83d62136b21f53"
sum="fe4a212f90e135049839a6ae056d9f37"
proved="true"
expanded="true"
shape="iapermut_allV2V6AasortedV6Aainfix &lt;=c0V0iiainfix &lt;ainfix -V10V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix =agetV7V11aTrueIainfix &lt;V11V0Aainfix &lt;V10V11FAainfix =agetV7V12aFalseIainfix &lt;V12V9Aainfix &lt;=c0V12FAapermut_allV2V8Aainfix &lt;V10V0Aainfix &lt;=c0V9Iainfix =V10ainfix -V3c1FIainfix =V9ainfix +V4c1FIaexchangeV6V8V4V3Aainfix &lt;=c0V0Lamk arrayV0V7FAainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4ainfix &lt;ainfix -V13V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix =agetV5V14aTrueIainfix &lt;V14V0Aainfix &lt;V13V14FAainfix =agetV5V15aFalseIainfix &lt;V15V4Aainfix &lt;=c0V15FAapermut_allV2V6Aainfix &lt;V13V0Aainfix &lt;=c0V4Iainfix =V13ainfix -V3c1Fainfix =agetV5V3aTrueAainfix &lt;V3V0Aainfix &lt;=c0V3ainfix &lt;ainfix -V3V16ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix =agetV5V17aTrueIainfix &lt;V17V0Aainfix &lt;V3V17FAainfix =agetV5V18aFalseIainfix &lt;V18V16Aainfix &lt;=c0V18FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V16Iainfix =V16ainfix +V4c1FNainfix =agetV5V4aTrueAainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0ainfix &lt;V4V3Iainfix =agetV5V19aTrueIainfix &lt;V19V0Aainfix &lt;V3V19FAainfix =agetV5V20aFalseIainfix &lt;V20V4Aainfix &lt;=c0V20FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FAainfix =agetV1V21aTrueIainfix &lt;V21V0Aainfix &lt;ainfix -V0c1V21FAainfix =agetV1V22aFalseIainfix &lt;V22c0Aainfix &lt;=c0V22FAapermut_allV2V2Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -47,9 +43,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="1. loop invariant init"
sum="57f0c0933b080490665b8d4a11257381"
sum="be337796f6ffb7138ea4eb638c7f16ab"
proved="true"
expanded="false"
expanded="true"
shape="loop invariant initainfix =agetV1V3aTrueIainfix &lt;V3V0Aainfix &lt;ainfix -V0c1V3FAainfix =agetV1V4aFalseIainfix &lt;V4c0Aainfix &lt;=c0V4FAapermut_allV2V2Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -67,9 +63,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="2. type invariant"
sum="ac8de2fc4a28fb385f99aea86a0db17b"
sum="8c36dae98d8df2a14052f6d61d34ef0d"
proved="true"
expanded="false"
expanded="true"
shape="type invariantainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -87,9 +83,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="3. index in array bounds"
sum="8f721b58ec5f964d028f3214f0476d12"
sum="3901c916b798294e334495c8db1624f3"
proved="true"
expanded="false"
expanded="true"
shape="index in array boundsainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -107,9 +103,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="4. loop invariant preservation"
sum="046e2e28f53002cf14ddb8a1b7888c12"
sum="ea65ebb39f6cbe989d2c5b5095093f54"
proved="true"
expanded="false"
expanded="true"
shape="loop invariant preservationainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V3V8FAainfix =agetV5V9aFalseIainfix &lt;V9V7Aainfix &lt;=c0V9FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V7Iainfix =V7ainfix +V4c1FINainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -127,9 +123,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="5. loop variant decrease"
sum="eafbcb3217f50272d46e034dea7c85d2"
sum="3658effca745b0fbf7207792246190a9"
proved="true"
expanded="false"
expanded="true"
shape="loop variant decreaseainfix &lt;ainfix -V3V7ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Iainfix =V7ainfix +V4c1FINainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V3V8FAainfix =agetV5V9aFalseIainfix &lt;V9V4Aainfix &lt;=c0V9FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -147,9 +143,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="6. index in array bounds"
sum="22f69edd7463058f47538beee1df2cde"
sum="55fafb6a05db1b860ea28160dcacf7a4"
proved="true"
expanded="false"
expanded="true"
shape="index in array boundsainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -167,9 +163,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="7. loop invariant preservation"
sum="18d1bad46f027314e3bcfb396ce80104"
sum="401bed39419a6ba6e91cfc6758d9e039"
proved="true"
expanded="false"
expanded="true"
shape="loop invariant preservationainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V7V8FAainfix =agetV5V9aFalseIainfix &lt;V9V4Aainfix &lt;=c0V9FAapermut_allV2V6Aainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V3c1FIainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -187,9 +183,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="8. loop variant decrease"
sum="877104df27c416ccefeb7b3fc83066ab"
sum="e6ea81f20fb557fb3eb41c0ce8297c51"
proved="true"
expanded="false"
expanded="true"
shape="loop variant decreaseainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Iainfix =V7ainfix -V3c1FIainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V3V8FAainfix =agetV5V9aFalseIainfix &lt;V9V4Aainfix &lt;=c0V9FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -207,9 +203,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="9. precondition"
sum="d1cc9d5e3abaa54b303e111cdb014b12"
sum="fa77dddc40c2b8f0effa4924ac6c7b66"
proved="true"
expanded="false"
expanded="true"
shape="preconditionainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4INainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -227,7 +223,7 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="10. loop invariant preservation"
sum="f2acb7b91794869d314a37f6fff10ba5"
sum="85108408d25b481d0b11eae7d49dc577"
proved="true"
expanded="true"
shape="loop invariant preservationainfix =agetV7V11aTrueIainfix &lt;V11V0Aainfix &lt;V10V11FAainfix =agetV7V12aFalseIainfix &lt;V12V9Aainfix &lt;=c0V12FAapermut_allV2V8Aainfix &lt;V10V0Aainfix &lt;=c0V9Iainfix =V10ainfix -V3c1FIainfix =V9ainfix +V4c1FIaexchangeV6V8V4V3Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4INainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V13aTrueIainfix &lt;V13V0Aainfix &lt;V3V13FAainfix =agetV5V14aFalseIainfix &lt;V14V4Aainfix &lt;=c0V14FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -242,9 +238,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="1."
sum="a8cfb95ae9097b417feab8f25ffe33de"
sum="781c26145a6bc032d2f1a89d6d008fee"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=c0V9Iainfix =V10ainfix -V3c1FIainfix =V9ainfix +V4c1FIaexchangeV6V8V4V3Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4INainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V11aTrueIainfix &lt;V11V0Aainfix &lt;V3V11FAainfix =agetV5V12aFalseIainfix &lt;V12V4Aainfix &lt;=c0V12FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -262,9 +258,9 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="2."
sum="3422959c95719e82c39211829abb3157"
sum="befb7b1134cb21cad589c70cc6cc7d12"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V10V0Iainfix =V10ainfix -V3c1FIainfix =V9ainfix +V4c1FIaexchangeV6V8V4V3Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4INainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V11aTrueIainfix &lt;V11V0Aainfix &lt;V3V11FAainfix =agetV5V12aFalseIainfix &lt;V12V4Aainfix &lt;=c0V12FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
......@@ -282,20 +278,19 @@
locfile="../vstte12_two_way_sort.mlw"
loclnum="22" loccnumb="6" loccnume="18"
expl="3."
sum="2b4043126e5e21b88b4f3a0afc98f5b3"
sum="7fb35de1a0a1005ca1ac992db430754c"
proved="true"
expanded="true"
shape="apermut_allV2V8Iainfix =V10ainfix -V3c1FIainfix =V9ainfix +V4c1FIaexchangeV6V8V4V3Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4INainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =agetV5V4aTrueIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V11aTrueIainfix &lt;V11V0Aainfix &lt;V3V11FAainfix =agetV5V12aFalseIainfix &lt;V12V4Aainfix &lt;=c0V12FAapermut_allV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for two_way_sort"/>
<proof
prover="3"
prover="1"
timelimit="10"
memlimit="1000"
edited="vstte12_two_way_sort_WP_TwoWaySort_WP_parameter_two_way_sort_2.v"
obsolete="false"
archived="false">
<result status="valid" time="1.12"/>
<result status="valid" time="0.06"/>