insertion_sort: updated proof

parent 398b9752
......@@ -6,11 +6,11 @@ Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
......@@ -26,11 +26,11 @@ Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
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).
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
......@@ -42,7 +42,7 @@ 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
......@@ -116,8 +116,8 @@ Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map 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), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))).
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 /\
......@@ -142,6 +142,12 @@ Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a))
(((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.
......@@ -156,13 +162,17 @@ Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)), (array_eq a1 a2) -> (permut a1 a2).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)),
let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z
Z)), forall (i:Z), ((1%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) ->
(((sorted_sub a3 0%Z i) /\ (permut (mk_array a a3) a2)) ->
(((sorted_sub a3 0%Z i) /\ (permut a2 (mk_array a a3))) ->
(((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a3 i) in forall (j:Z),
forall (a4:(map Z Z)), let a5 := (mk_array a a4) in ((((0%Z <= j)%Z /\
(j <= i)%Z) /\ ((permut (set1 a5 j result) a2) /\ ((forall (k1:Z) (k2:Z),
(j <= i)%Z) /\ ((permut a2 (set1 a5 j result)) /\ ((forall (k1:Z) (k2:Z),
(((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> ((~ (k1 = j)) ->
((~ (k2 = j)) -> ((get a4 k1) <= (get a4 k2))%Z))) /\ forall (k:Z),
(((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a4 k))%Z))) ->
......@@ -170,13 +180,13 @@ Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)),
((result < (get a4 (j - 1%Z)%Z))%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\
((j - 1%Z)%Z < a)%Z) -> (((0%Z <= j)%Z /\ (j < a)%Z) -> forall (a6:(map Z
Z)), let a7 := (mk_array a a6) in ((a6 = (set a4 j (get a4
(j - 1%Z)%Z))) -> ((exchange match (set1 a7 (j - 1%Z)%Z
(j - 1%Z)%Z))) -> ((exchange match (set1 a5 j
result) with
| mk_array _ elts1 => elts1
end match (set1 a5 j result) with
end match (set1 a7 (j - 1%Z)%Z result) with
| mk_array _ elts1 => elts1
end (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut (set1 a7
j1 result) a2)))))))))))).
end (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2
(set1 a7 j1 result))))))))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
......@@ -190,12 +200,12 @@ subst a6.
simpl.
apply permut_trans with (elts (set1 (mk_array a a4) j (get a3 i))); auto.
subst j1.
unfold permut in H12.
intuition.
apply permut_exchange with (j-1)%Z j.
simpl; omega.
simpl; omega.
assumption.
unfold permut in H12.
intuition.
subst j1; assumption.
Qed.
(* DO NOT EDIT BELOW *)
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="../insertion_sort/why3session.xml">
<why3session name="examples/programs/insertion_sort/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="yices" name="Yices" version="1.0.27"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../insertion_sort.mlw" verified="false" expanded="true">
<theory name="WP InsertionSort" verified="false" expanded="true">
<goal name="WP_parameter insertion_sort" expl="correctness of parameter insertion_sort" sum="ba7d33cff433c31f31822790e3c8b75e" proved="false" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3apermutV2V4AasortedV4IapermutV2V4Aasorted_subV3c0ainfix +ainfix -V0c1c1ALagetV3V5Lamk arrayV0V8iainfix >V7c0iainfix >agetV8ainfix -V7c1V6Lamk arrayV0V10ainfix <V12V7Aainfix <=c0V7Aainfix <V6agetV10V13Iainfix <=V13V5Aainfix <=ainfix +V12c1V13FAainfix <=agetV10V14agetV10V15Iainfix =V15V12NIainfix =V14V12NIainfix <=V15V5Aainfix <=V14V15Aainfix <=c0V14FAapermutV2asetV11V12V6Aainfix <=V12V5Aainfix <=c0V12Iainfix =V12ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV16CasetV11ainfix -V7c1V6amk arraywVV17ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V18Aasorted_subV18c0ainfix +V5c1Iainfix =V18asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V19V6Iainfix <V19V7Aainfix <=c0V19FAainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1ifLamk arrayV0V20ainfix <V22V7Aainfix <=c0V7Aainfix <V6agetV20V23Iainfix <=V23V5Aainfix <=ainfix +V22c1V23FAainfix <=agetV20V24agetV20V25Iainfix =V25V22NIainfix =V24V22NIainfix <=V25V5Aainfix <=V24V25Aainfix <=c0V24FAapermutV2asetV21V22V6Aainfix <=V22V5Aainfix <=c0V22Iainfix =V22ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV26CasetV21ainfix -V7c1V6amk arraywVV27ainfix -V7c1V7Iainfix =V20asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V28Aasorted_subV28c0ainfix +V5c1Iainfix =V28asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V29V6Iainfix <V29V7Aainfix <=c0V29FIainfix <V6agetV8V30Iainfix <=V30V5Aainfix <=ainfix +V7c1V30FAainfix <=agetV8V31agetV8V32Iainfix =V32V7NIainfix =V31V7NIainfix <=V32V5Aainfix <=V31V32Aainfix <=c0V31FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFAainfix <V6agetV3V33Iainfix <=V33V5Aainfix <=ainfix +V5c1V33FAainfix <=agetV3V34agetV3V35Iainfix =V35V5NIainfix =V34V5NIainfix <=V35V5Aainfix <=V34V35Aainfix <=c0V34FAapermutV2asetV4V5V6Aainfix <=V5V5Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFAapermutV2V2Aasorted_subV1c0c1Iainfix <=c1ainfix -V0c1AapermutV2V2AasortedV2Iainfix >c1ainfix -V0c1FF">
<transf name="split_goal" proved="false" expanded="true">
<file name="../insertion_sort.mlw" verified="true" expanded="true">
<theory name="WP InsertionSort" verified="true" expanded="true">
<goal name="WP_parameter insertion_sort" expl="correctness of parameter insertion_sort" sum="ba7d33cff433c31f31822790e3c8b75e" proved="true" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3apermutV2V4AasortedV4IapermutV2V4Aasorted_subV3c0ainfix +ainfix -V0c1c1ALagetV3V5Lamk arrayV0V8iainfix >V7c0iainfix >agetV8ainfix -V7c1V6Lamk arrayV0V10ainfix <V12V7Aainfix <=c0V7Aainfix <V6agetV10V13Iainfix <=V13V5Aainfix <=ainfix +V12c1V13FAainfix <=agetV10V14agetV10V15Iainfix =V15V12NIainfix =V14V12NIainfix <=V15V5Aainfix <=V14V15Aainfix <=c0V14FAapermutV2asetV11V12V6Aainfix <=V12V5Aainfix <=c0V12Iainfix =V12ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV16CasetV11ainfix -V7c1V6amk arraywVV17ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V18Aasorted_subV18c0ainfix +V5c1Iainfix =V18asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V19V6Iainfix <V19V7Aainfix <=c0V19FAainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1ifLamk arrayV0V20ainfix <V22V7Aainfix <=c0V7Aainfix <V6agetV20V23Iainfix <=V23V5Aainfix <=ainfix +V22c1V23FAainfix <=agetV20V24agetV20V25Iainfix =V25V22NIainfix =V24V22NIainfix <=V25V5Aainfix <=V24V25Aainfix <=c0V24FAapermutV2asetV21V22V6Aainfix <=V22V5Aainfix <=c0V22Iainfix =V22ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV26CasetV21ainfix -V7c1V6amk arraywVV27ainfix -V7c1V7Iainfix =V20asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V28Aasorted_subV28c0ainfix +V5c1Iainfix =V28asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V29V6Iainfix <V29V7Aainfix <=c0V29FIainfix <V6agetV8V30Iainfix <=V30V5Aainfix <=ainfix +V7c1V30FAainfix <=agetV8V31agetV8V32Iainfix =V32V7NIainfix =V31V7NIainfix <=V32V5Aainfix <=V31V32Aainfix <=c0V31FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFAainfix <V6agetV3V33Iainfix <=V33V5Aainfix <=ainfix +V5c1V33FAainfix <=agetV3V34agetV3V35Iainfix =V35V5NIainfix =V34V5NIainfix <=V35V5Aainfix <=V34V35Aainfix <=c0V34FAapermutV2asetV4V5V6Aainfix <=V5V5Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFAapermutV2V2Aasorted_subV1c0c1Iainfix <=c1ainfix -V0c1AapermutV2V2AasortedV2Iainfix >c1ainfix -V0c1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.1" expl="normal postcondition" sum="0d467139981e2be12600aa9eab9b5387" proved="true" expanded="true" shape="Lamk arrayV0V1apermutV2V2AasortedV2Iainfix >c1ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.04"/>
......@@ -42,8 +39,8 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter insertion_sort.3" expl="for loop preservation" sum="93d44998908e8b7fcdc34c21cede0f4f" proved="false" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8iainfix >V7c0iainfix >agetV8ainfix -V7c1V6Lamk arrayV0V10ainfix <V12V7Aainfix <=c0V7Aainfix <V6agetV10V13Iainfix <=V13V5Aainfix <=ainfix +V12c1V13FAainfix <=agetV10V14agetV10V15Iainfix =V15V12NIainfix =V14V12NIainfix <=V15V5Aainfix <=V14V15Aainfix <=c0V14FAapermutV2asetV11V12V6Aainfix <=V12V5Aainfix <=c0V12Iainfix =V12ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV16CasetV11ainfix -V7c1V6amk arraywVV17ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V18Aasorted_subV18c0ainfix +V5c1Iainfix =V18asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V19V6Iainfix <V19V7Aainfix <=c0V19FAainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1ifLamk arrayV0V20ainfix <V22V7Aainfix <=c0V7Aainfix <V6agetV20V23Iainfix <=V23V5Aainfix <=ainfix +V22c1V23FAainfix <=agetV20V24agetV20V25Iainfix =V25V22NIainfix =V24V22NIainfix <=V25V5Aainfix <=V24V25Aainfix <=c0V24FAapermutV2asetV21V22V6Aainfix <=V22V5Aainfix <=c0V22Iainfix =V22ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV26CasetV21ainfix -V7c1V6amk arraywVV27ainfix -V7c1V7Iainfix =V20asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V28Aasorted_subV28c0ainfix +V5c1Iainfix =V28asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V29V6Iainfix <V29V7Aainfix <=c0V29FIainfix <V6agetV8V30Iainfix <=V30V5Aainfix <=ainfix +V7c1V30FAainfix <=agetV8V31agetV8V32Iainfix =V32V7NIainfix =V31V7NIainfix <=V32V5Aainfix <=V31V32Aainfix <=c0V31FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFAainfix <V6agetV3V33Iainfix <=V33V5Aainfix <=ainfix +V5c1V33FAainfix <=agetV3V34agetV3V35Iainfix =V35V5NIainfix =V34V5NIainfix <=V35V5Aainfix <=V34V35Aainfix <=c0V34FAapermutV2asetV4V5V6Aainfix <=V5V5Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter insertion_sort.3" expl="for loop preservation" sum="93d44998908e8b7fcdc34c21cede0f4f" proved="true" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8iainfix >V7c0iainfix >agetV8ainfix -V7c1V6Lamk arrayV0V10ainfix <V12V7Aainfix <=c0V7Aainfix <V6agetV10V13Iainfix <=V13V5Aainfix <=ainfix +V12c1V13FAainfix <=agetV10V14agetV10V15Iainfix =V15V12NIainfix =V14V12NIainfix <=V15V5Aainfix <=V14V15Aainfix <=c0V14FAapermutV2asetV11V12V6Aainfix <=V12V5Aainfix <=c0V12Iainfix =V12ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV16CasetV11ainfix -V7c1V6amk arraywVV17ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V18Aasorted_subV18c0ainfix +V5c1Iainfix =V18asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V19V6Iainfix <V19V7Aainfix <=c0V19FAainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1ifLamk arrayV0V20ainfix <V22V7Aainfix <=c0V7Aainfix <V6agetV20V23Iainfix <=V23V5Aainfix <=ainfix +V22c1V23FAainfix <=agetV20V24agetV20V25Iainfix =V25V22NIainfix =V24V22NIainfix <=V25V5Aainfix <=V24V25Aainfix <=c0V24FAapermutV2asetV21V22V6Aainfix <=V22V5Aainfix <=c0V22Iainfix =V22ainfix -V7c1FAaexchangeCasetV9V7V6amk arraywVV26CasetV21ainfix -V7c1V6amk arraywVV27ainfix -V7c1V7Iainfix =V20asetV8V7agetV8ainfix -V7c1FAainfix <V7V0Aainfix <=c0V7Aainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1apermutV2amk arrayV0V28Aasorted_subV28c0ainfix +V5c1Iainfix =V28asetV8V7V6FAainfix <V7V0Aainfix <=c0V7Aainfix <=agetV8V29V6Iainfix <V29V7Aainfix <=c0V29FIainfix <V6agetV8V30Iainfix <=V30V5Aainfix <=ainfix +V7c1V30FAainfix <=agetV8V31agetV8V32Iainfix =V32V7NIainfix =V31V7NIainfix <=V32V5Aainfix <=V31V32Aainfix <=c0V31FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFAainfix <V6agetV3V33Iainfix <=V33V5Aainfix <=ainfix +V5c1V33FAainfix <=agetV3V34agetV3V35Iainfix =V35V5NIainfix =V34V5NIainfix <=V35V5Aainfix <=V34V35Aainfix <=c0V34FAapermutV2asetV4V5V6Aainfix <=V5V5Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.3.1" expl="for loop preservation" sum="26d6c7b5d446796ede5132f4c6e6cf56" proved="true" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3ainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
......@@ -89,8 +86,8 @@
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7" expl="for loop preservation" sum="07de9781228b48c01d77f6fee2500e9c" proved="false" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8Lamk arrayV0V10ainfix <V6agetV10V13Iainfix <=V13V5Aainfix <=ainfix +V12c1V13FAainfix <=agetV10V14agetV10V15Iainfix =V15V12NIainfix =V14V12NIainfix <=V15V5Aainfix <=V14V15Aainfix <=c0V14FAapermutV2asetV11V12V6Aainfix <=V12V5Aainfix <=c0V12Iainfix =V12ainfix -V7c1FIaexchangeCasetV9V7V6amk arraywVV16CasetV11ainfix -V7c1V6amk arraywVV17ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FIainfix <V7V0Aainfix <=c0V7Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >agetV8ainfix -V7c1V6Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >V7c0Iainfix <V6agetV8V18Iainfix <=V18V5Aainfix <=ainfix +V7c1V18FAainfix <=agetV8V19agetV8V20Iainfix =V20V7NIainfix =V19V7NIainfix <=V20V5Aainfix <=V19V20Aainfix <=c0V19FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFIainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter insertion_sort.3.7" expl="for loop preservation" sum="07de9781228b48c01d77f6fee2500e9c" proved="true" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8Lamk arrayV0V10ainfix <V6agetV10V13Iainfix <=V13V5Aainfix <=ainfix +V12c1V13FAainfix <=agetV10V14agetV10V15Iainfix =V15V12NIainfix =V14V12NIainfix <=V15V5Aainfix <=V14V15Aainfix <=c0V14FAapermutV2asetV11V12V6Aainfix <=V12V5Aainfix <=c0V12Iainfix =V12ainfix -V7c1FIaexchangeCasetV9V7V6amk arraywVV16CasetV11ainfix -V7c1V6amk arraywVV17ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FIainfix <V7V0Aainfix <=c0V7Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >agetV8ainfix -V7c1V6Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >V7c0Iainfix <V6agetV8V18Iainfix <=V18V5Aainfix <=ainfix +V7c1V18FAainfix <=agetV8V19agetV8V20Iainfix =V20V7NIainfix =V19V7NIainfix <=V20V5Aainfix <=V19V20Aainfix <=c0V19FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFIainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.3.7.1" expl="for loop preservation" sum="67b6e80fae5e80dbfd7a026b263d88d5" proved="true" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8Lamk arrayV0V10ainfix <=c0V12Iainfix =V12ainfix -V7c1FIaexchangeCasetV9V7V6amk arraywVV13CasetV11ainfix -V7c1V6amk arraywVV14ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FIainfix <V7V0Aainfix <=c0V7Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >agetV8ainfix -V7c1V6Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >V7c0Iainfix <V6agetV8V15Iainfix <=V15V5Aainfix <=ainfix +V7c1V15FAainfix <=agetV8V16agetV8V17Iainfix =V17V7NIainfix =V16V7NIainfix <=V17V5Aainfix <=V16V17Aainfix <=c0V16FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFIainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
......@@ -107,18 +104,9 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.3" expl="for loop preservation" sum="d151c246094fcbaee0d63f8daf0daac4" proved="false" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8Lamk arrayV0V10apermutV2asetV11V12V6Iainfix =V12ainfix -V7c1FIaexchangeCasetV9V7V6amk arraywVV13CasetV11ainfix -V7c1V6amk arraywVV14ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FIainfix <V7V0Aainfix <=c0V7Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >agetV8ainfix -V7c1V6Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >V7c0Iainfix <V6agetV8V15Iainfix <=V15V5Aainfix <=ainfix +V7c1V15FAainfix <=agetV8V16agetV8V17Iainfix =V17V7NIainfix =V16V7NIainfix <=V17V5Aainfix <=V16V17Aainfix <=c0V16FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFIainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<goal name="WP_parameter insertion_sort.3.7.3" expl="for loop preservation" sum="d151c246094fcbaee0d63f8daf0daac4" proved="true" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8Lamk arrayV0V10apermutV2asetV11V12V6Iainfix =V12ainfix -V7c1FIaexchangeCasetV9V7V6amk arraywVV13CasetV11ainfix -V7c1V6amk arraywVV14ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FIainfix <V7V0Aainfix <=c0V7Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >agetV8ainfix -V7c1V6Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >V7c0Iainfix <V6agetV8V15Iainfix <=V15V5Aainfix <=ainfix +V7c1V15FAainfix <=agetV8V16agetV8V17Iainfix =V17V7NIainfix =V16V7NIainfix <=V17V5Aainfix <=V16V17Aainfix <=c0V16FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFIainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
<proof prover="coq" timelimit="10" edited="insertion_sort_WP_InsertionSort_WP_parameter_insertion_sort_1.v" obsolete="false">
<result status="unknown" time="0.53"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="11.66"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.13"/>
<result status="valid" time="0.82"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.4" expl="for loop preservation" sum="4249a7d0a8e06086ba18245ad25240b8" proved="true" expanded="true" shape="Lamk arrayV0V1Lamk arrayV0V3LagetV3V5Lamk arrayV0V8Lamk arrayV0V10ainfix <=agetV10V13agetV10V14Iainfix =V14V12NIainfix =V13V12NIainfix <=V14V5Aainfix <=V13V14Aainfix <=c0V13FIainfix =V12ainfix -V7c1FIaexchangeCasetV9V7V6amk arraywVV15CasetV11ainfix -V7c1V6amk arraywVV16ainfix -V7c1V7Iainfix =V10asetV8V7agetV8ainfix -V7c1FIainfix <V7V0Aainfix <=c0V7Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >agetV8ainfix -V7c1V6Iainfix <ainfix -V7c1V0Aainfix <=c0ainfix -V7c1Iainfix >V7c0Iainfix <V6agetV8V17Iainfix <=V17V5Aainfix <=ainfix +V7c1V17FAainfix <=agetV8V18agetV8V19Iainfix =V19V7NIainfix =V18V7NIainfix <=V19V5Aainfix <=V18V19Aainfix <=c0V18FAapermutV2asetV9V7V6Aainfix <=V7V5Aainfix <=c0V7FFIainfix <V5V0Aainfix <=c0V5IapermutV2V4Aasorted_subV3c0V5Iainfix <=V5ainfix -V0c1Aainfix <=c1V5FFIainfix <=c1ainfix -V0c1FF">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment