Commit a46145bb authored by MARCHE Claude's avatar MARCHE Claude

updated failed sessions

parent 3c6e55ad
......@@ -360,7 +360,7 @@
locfile="../blocking_semantics5.mlw"
loclnum="358" loccnumb="7" loccnume="25"
verified="true"
expanded="false">
expanded="true">
<goal
name="type_inversion"
locfile="../blocking_semantics5.mlw"
......@@ -480,12 +480,12 @@
loclnum="385" loccnumb="6" loccnume="20"
sum="ef45c8c0c4ea0692ce4d29abba57f1ab"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =atype_valueaeval_termV1V2V0V5Iatype_termV3V4V0V5Iacompatible_envV1V3V2V4F">
<transf
name="induction_ty_lex"
proved="true"
expanded="false">
expanded="true">
<goal
name="eval_type_term.1"
locfile="../blocking_semantics5.mlw"
......@@ -493,12 +493,12 @@
expl="1."
sum="da19ffa623b601c2a1ed0be1144512f3"
proved="true"
expanded="false"
expanded="true"
shape="Cainfix =atype_valueaeval_termV2V3V0V6Iatype_termV4V5V0V6Iacompatible_envV2V4V3V5FaTvalueVainfix =atype_valueaeval_termV8V9V0V12Iatype_termV10V11V0V12Iacompatible_envV8V10V9V11FaTvarVainfix =atype_valueaeval_termV14V15V0V18Iatype_termV16V17V0V18Iacompatible_envV14V16V15V17FaTderefVainfix =atype_valueaeval_termV22V23V0V26Iatype_termV24V25V0V26Iacompatible_envV22V24V23V25FIainfix =atype_valueaeval_termV27V28V19V31Iatype_termV29V30V19V31Iacompatible_envV27V29V28V30FIainfix =atype_valueaeval_termV32V33V21V36Iatype_termV34V35V21V36Iacompatible_envV32V34V33V35FaTbinVVVV0F">
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="eval_type_term.1.1"
locfile="../blocking_semantics5.mlw"
......@@ -656,7 +656,7 @@
expl="4."
sum="27b28225019b2f44a6cb684ea7896ffe"
proved="true"
expanded="false"
expanded="true"
shape="CtaTvalueVtaTvarVtaTderefVainfix =atype_valueaeval_termV7V8V0V11Iatype_termV9V10V0V11Iacompatible_envV7V9V8V10FIainfix =atype_valueaeval_termV12V13V4V16Iatype_termV14V15V4V16Iacompatible_envV12V14V13V15FIainfix =atype_valueaeval_termV17V18V6V21Iatype_termV19V20V6V21Iacompatible_envV17V19V18V20FaTbinVVVV0F">
<proof
prover="0"
......@@ -666,14 +666,6 @@
archived="false">
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="4.47"/>
</proof>
<proof
prover="2"
timelimit="5"
......
......@@ -2487,14 +2487,14 @@
expl="VC for downsweep"
sum="0627af2a942dafa940d6138cfdba6009"
proved="true"
expanded="false"
expanded="true"
shape="iainfix =agetV9V11agetV5V11Iainfix &gt;V11V1FAainfix =agetV9V12agetV5V12Iainfix &lt;=V12ainfix -V0ainfix -V1V0FAapartial_sumV0V1V7V10ainfix =agetV18V20agetV5V20Iainfix &gt;V20V1FAainfix =agetV18V21agetV5V21Iainfix &lt;=V21ainfix -V0ainfix -V1V0FAapartial_sumV0V1V7V19Aapartial_sumainfix -V1adivV13c2V1V7V19Aapartial_sumainfix -V0adivV13c2V0V7V19Iainfix =agetV18V22agetV15V22Iainfix &gt;V22V1FAainfix =agetV18V23agetV15V23Iainfix &lt;=V23ainfix -V17ainfix -V1V17FAapartial_sumV17V1V7V19Aainfix &lt;=c0V4Lamk arrayV4V18FAaphase1V17V1V7V16Aainfix =agetV15V1asumV3c0ainfix +ainfix -V17ainfix -V1V17c1Aais_power_of_2ainfix -V1V17Aainfix &lt;=aprefix -c1ainfix -V17ainfix -V1V17Aainfix &lt;V1V4Aainfix &lt;V17V1Aainfix &lt;=c0V17Lainfix -V1adivV13c2Aaphase1ago_rightV0V1V1V7V16Iainfix =agetV15V24agetV9V24Iainfix &gt;V24V0FAainfix =agetV15V25agetV9V25Iainfix &lt;=V25ainfix -V14ainfix -V0V14FAapartial_sumV14V0V7V16Aainfix &lt;=c0V4Lamk arrayV4V15FAaphase1V14V0V7V10Aainfix =agetV9V0asumV3c0ainfix +ainfix -V14ainfix -V0V14c1Aais_power_of_2ainfix -V0V14Aainfix &lt;=aprefix -c1ainfix -V14ainfix -V0V14Aainfix &lt;V0V4Aainfix &lt;V14V0Aainfix &lt;=c0V14Lainfix -V0adivV13c2Aaphase1ago_rightV0V1V1V7V10Aaphase1ago_rightV0V1V1V7V6Aaphase1ago_leftV0V1V0V7V6Lainfix -V1V0ainfix &gt;V1ainfix +V0c1Aainfix =agetV9V1asumV3c0ainfix +V0c1Iainfix =V9asetV8V0agetV5V1Aainfix &lt;=c0V4Lamk arrayV4V9FAainfix &lt;V0V4Aainfix &lt;=c0V0Iainfix =V8asetV5V1ainfix +agetV5V1agetV5V0Aainfix &lt;=c0V4FAainfix &lt;V1V4Aainfix &lt;=c0V1Aainfix &lt;V1V4Aainfix &lt;=c0V1Aainfix &lt;V0V4Aainfix &lt;=c0V0Aainfix =agetV5V0asumV3ainfix +ainfix -V0ainfix -V1V0c1ainfix +V0c1Aainfix =agetV5V1asumV3c0ainfix +ainfix -V0ainfix -V1V0c1Aainfix &lt;V1V4Aainfix &lt;=c0V1Iaphase1V0V1V7V6Aainfix =agetV5V1asumV3c0ainfix +ainfix -V0ainfix -V1V0c1Aais_power_of_2ainfix -V1V0Aainfix &lt;=aprefix -c1ainfix -V0ainfix -V1V0Aainfix &lt;V1V4Aainfix &lt;V0V1Aainfix &lt;=c0V0Aainfix &lt;=c0V4Aainfix &lt;=c0V2Lamk arrayV2V3Lamk arrayV4V5F">
<label
name="expl:VC for downsweep"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter downsweep.1"
locfile="../verifythis_PrefixSumRec.mlw"
......@@ -3590,7 +3590,7 @@
expl="17. assertion"
sum="25e9bb8b200c941ab38b44ae626dae4a"
proved="true"
expanded="false"
expanded="true"
shape="assertionaphase1ago_rightV0V1V1V7V14Iainfix =agetV13V15agetV9V15Iainfix &gt;V15V0FAainfix =agetV13V16agetV9V16Iainfix &lt;=V16ainfix -V12ainfix -V0V12FAapartial_sumV12V0V7V14Aainfix &lt;=c0V4Lamk arrayV4V13FIaphase1V12V0V7V10Aainfix =agetV9V0asumV3c0ainfix +ainfix -V12ainfix -V0V12c1Aais_power_of_2ainfix -V0V12Aainfix &lt;=aprefix -c1ainfix -V12ainfix -V0V12Aainfix &lt;V0V4Aainfix &lt;V12V0Aainfix &lt;=c0V12Lainfix -V0adivV11c2Iaphase1ago_rightV0V1V1V7V10Iaphase1ago_rightV0V1V1V7V6Iaphase1ago_leftV0V1V0V7V6Lainfix -V1V0Iainfix &gt;V1ainfix +V0c1Iainfix =agetV9V1asumV3c0ainfix +V0c1Iainfix =V9asetV8V0agetV5V1Aainfix &lt;=c0V4Lamk arrayV4V9FIainfix &lt;V0V4Aainfix &lt;=c0V0Iainfix =V8asetV5V1ainfix +agetV5V1agetV5V0Aainfix &lt;=c0V4FIainfix &lt;V1V4Aainfix &lt;=c0V1Iainfix &lt;V1V4Aainfix &lt;=c0V1Iainfix &lt;V0V4Aainfix &lt;=c0V0Iainfix =agetV5V0asumV3ainfix +ainfix -V0ainfix -V1V0c1ainfix +V0c1Iainfix =agetV5V1asumV3c0ainfix +ainfix -V0ainfix -V1V0c1Iainfix &lt;V1V4Aainfix &lt;=c0V1Iaphase1V0V1V7V6Aainfix =agetV5V1asumV3c0ainfix +ainfix -V0ainfix -V1V0c1Aais_power_of_2ainfix -V1V0Aainfix &lt;=aprefix -c1ainfix -V0ainfix -V1V0Aainfix &lt;V1V4Aainfix &lt;V0V1Aainfix &lt;=c0V0Aainfix &lt;=c0V4Aainfix &lt;=c0V2Lamk arrayV2V3Lamk arrayV4V5F">
<label
name="expl:VC for downsweep"/>
......@@ -3626,14 +3626,6 @@
archived="false">
<result status="timeout" time="29.82"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="26.01"/>
</proof>
<proof
prover="5"
timelimit="30"
......
......@@ -220,14 +220,14 @@
expl="VC for lcp"
sum="9313b54ae999fadb10c70710bfa1cb0a"
proved="true"
expanded="false"
expanded="true"
shape="iais_longest_common_prefixV4V2V3V5iais_longest_common_prefixV4V2V3V5iais_longest_common_prefixV4V2V3V5ais_common_prefixV4V2V3V8Iainfix =V8ainfix +V5c1Fainfix =agetV1V7agetV1V6Aainfix &lt;V7V0Aainfix &lt;=c0V7Lainfix +V2V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5ainfix &lt;ainfix +V3V5V0ainfix &lt;ainfix +V2V5V0Iais_common_prefixV4V2V3V5FAais_common_prefixV4V2V3c0Iainfix &lt;=V3V0Aainfix &lt;=c0V3Aainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for lcp"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter lcp.1"
locfile="../verifythis_fm2012_LRS.mlw"
......@@ -487,7 +487,7 @@
expl="4. loop invariant preservation"
sum="52ae9361015a2fd5d317e9cfc96f121c"
proved="true"
expanded="false"
expanded="true"
shape="loop invariant preservationais_common_prefixV4V2V3V8Iainfix =V8ainfix +V5c1FIainfix =agetV1V7agetV1V6Iainfix &lt;V7V0Aainfix &lt;=c0V7Lainfix +V2V5Iainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0Iais_common_prefixV4V2V3V5FIainfix &lt;=V3V0Aainfix &lt;=c0V3Aainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for lcp"/>
......@@ -3772,7 +3772,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="5"
......@@ -3780,7 +3780,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="6.78"/>
<result status="valid" time="7.32"/>
</proof>
<proof
prover="6"
......@@ -3788,7 +3788,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.20"/>
<result status="valid" time="0.21"/>
</proof>
<proof
prover="7"
......@@ -3796,7 +3796,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="8"
......@@ -3804,7 +3804,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="9"
......@@ -3856,7 +3856,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
......@@ -3864,7 +3864,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="7.32"/>
<result status="valid" time="6.78"/>
</proof>
<proof
prover="6"
......@@ -3872,7 +3872,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
<result status="valid" time="0.20"/>
</proof>
<proof
prover="7"
......@@ -3880,7 +3880,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="8"
......@@ -3888,7 +3888,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="9"
......@@ -5010,14 +5010,6 @@
archived="false">
<result status="valid" time="1.08"/>
</proof>
<proof
prover="1"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
</proof>
<proof
prover="2"
timelimit="10"
......@@ -5755,7 +5747,7 @@
locfile="../verifythis_fm2012_LRS.mlw"
loclnum="288" loccnumb="7" loccnume="18"
verified="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter select"
locfile="../verifythis_fm2012_LRS.mlw"
......@@ -5856,14 +5848,6 @@
archived="false">
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="1"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
</proof>
<proof
prover="2"
timelimit="10"
......@@ -7130,14 +7114,14 @@
expl="VC for lcp"
sum="ca9616c67763bf8ea361ba4eb50c381c"
proved="true"
expanded="false"
expanded="true"
shape="ais_longest_common_prefixamk arrayV0V1agetV3ainfix -V4c1agetV3V4V8Iais_longest_common_prefixamk arrayV0V1V7V6V8FAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;=V7V0Aainfix &lt;=c0V7LagetV3V4Aainfix &lt;V4V2Aainfix &lt;=c0V4LagetV3V5Aainfix &lt;V5V2Aainfix &lt;=c0V5Lainfix -V4c1Iainfix &lt;V4V0Aainfix &lt;c0V4Aainfix &lt;=c0V2Aainfix &lt;=c0V0Aasorted_subamk arrayV0V1V3c0V2AapermutationV3V2Aainfix =V0V2F">
<label
name="expl:VC for lcp"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter lcp.1"
locfile="../verifythis_fm2012_LRS.mlw"
......@@ -7323,7 +7307,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -7339,7 +7323,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="3"
......@@ -7355,7 +7339,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="9.96"/>
<result status="timeout" time="9.98"/>
</proof>
<proof
prover="6"
......@@ -7397,7 +7381,7 @@
expl="4. precondition"
sum="d6e3e017e9e84315aab8d4adf70dd0db"
proved="true"
expanded="false"
expanded="true"
shape="preconditionainfix &lt;=V6V0Aainfix &lt;=c0V6LagetV3V4Iainfix &lt;V4V2Aainfix &lt;=c0V4LagetV3V5Iainfix &lt;V5V2Aainfix &lt;=c0V5Lainfix -V4c1Iainfix &lt;V4V0Aainfix &lt;c0V4Aainfix &lt;=c0V2Aainfix &lt;=c0V0Aasorted_subamk arrayV0V1V3c0V2AapermutationV3V2Aainfix =V0V2F">
<label
name="expl:VC for lcp"/>
......@@ -7407,7 +7391,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -7423,7 +7407,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
......@@ -7439,15 +7423,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="9.98"/>
</proof>
<proof
prover="6"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.45"/>
<result status="timeout" time="9.96"/>
</proof>
<proof
prover="7"
......
......@@ -187,7 +187,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.58"/>
<result status="valid" time="2.96"/>
</proof>
</goal>
<goal
......@@ -856,7 +856,7 @@
prover="0"
timelimit="5"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="4.95"/>
</proof>
......
(* 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 list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Nth.
Require option.Option.
Require list.NthLength.
Require list.Append.
Require list.NthLengthAppend.
(* 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 *)
Inductive buffer
(a:Type) {a_WT:WhyType a} :=
| mk_buffer : Z -> Z -> (@array a a_WT) -> (list a) -> buffer a.
Axiom buffer_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (buffer a).
Existing Instance buffer_WhyType.
Implicit Arguments mk_buffer [[a] [a_WT]].
(* Why3 assumption *)
Definition sequence {a:Type} {a_WT:WhyType a} (v:(@buffer
a a_WT)): (list a) := match v with
| (mk_buffer x x1 x2 x3) => x3
end.
(* Why3 assumption *)
Definition data {a:Type} {a_WT:WhyType a} (v:(@buffer a a_WT)): (@array
a a_WT) := match v with
| (mk_buffer x x1 x2 x3) => x2
end.
(* Why3 assumption *)
Definition len {a:Type} {a_WT:WhyType a} (v:(@buffer a a_WT)): Z :=
match v with
| (mk_buffer x x1 x2 x3) => x1
end.
(* Why3 assumption *)
Definition first {a:Type} {a_WT:WhyType a} (v:(@buffer a a_WT)): Z :=
match v with
| (mk_buffer x x1 x2 x3) => x
end.
(* Why3 assumption *)
Definition size {a:Type} {a_WT:WhyType a} (b:(@buffer a a_WT)): Z :=
(length (data b)).
(* Why3 goal *)
Theorem WP_parameter_pop : forall {a:Type} {a_WT:WhyType a}, forall (b:Z)
(b1:Z) (b2:Z) (b3:(@map.Map.map Z _ a a_WT)) (b4:(list a)),
(((((0%Z <= b)%Z /\ (b < b2)%Z) /\ (((0%Z <= b1)%Z /\ (b1 <= b2)%Z) /\
((b1 = (list.Length.length b4)) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < b1)%Z) -> ((((b + i)%Z < b2)%Z -> ((list.Nth.nth i
b4) = (Some (map.Map.get b3 (b + i)%Z)))) /\
((0%Z <= ((b + i)%Z - b2)%Z)%Z -> ((list.Nth.nth i
b4) = (Some (map.Map.get b3 ((b + i)%Z - b2)%Z)))))))) /\ (0%Z <= b2)%Z) /\
(0%Z < b1)%Z) ->
match b4 with
| nil => True
| (cons _ s) => forall (rho:(list a)), (rho = s) -> (((0%Z <= b)%Z /\
(b < b2)%Z) -> forall (rho1:Z), (rho1 = (b1 - 1%Z)%Z) ->
forall (rho2:Z), (rho2 = (b + 1%Z)%Z) -> ((~ (rho2 = b2)) ->
forall (i:Z), ((0%Z <= i)%Z /\ (i < rho1)%Z) ->
((0%Z <= ((rho2 + i)%Z - b2)%Z)%Z -> ((list.Nth.nth i
rho) = (Some (map.Map.get b3 ((rho2 + i)%Z - b2)%Z))))))
end.
intros a a_WT b b1 b2 b3 b4 ((((h1,h2),((h3,h4),(h5,h6))),h7),h8).
destruct b4; auto.
intros r H H1; subst r.
intros r H; subst r.
intros r H H2; subst r.
intros i H3 H4.
assert (h: (0 <= i+1 < b1)%Z) by omega.
generalize (h6 (i+1)%Z h).
Require Import Why3.
why3 "alt-ergo".
Qed.
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