MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 9d99326f authored by Martin Clochard's avatar Martin Clochard
Browse files

Theory of sequences: seq is always infinite

parent e0467a30
......@@ -2,12 +2,12 @@
<!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.2" timelimit="6" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<file name="../verifythis_2015_dancing_links.mlw" expanded="true">
<theory name="DancingLinks" sum="9ccd1c1f1172efa1e75be2e365507169" expanded="true">
<goal name="WP_parameter remove" expl="VC for remove" expanded="true">
<theory name="DancingLinks" sum="79590f88b910b806d8e4109777ab8ee7" expanded="true">
<goal name="WP_parameter remove" expl="VC for remove">
<transf name="split_goal_wp">
<goal name="WP_parameter remove.1" expl="1. index in array bounds">
<proof prover="1"><result status="valid" time="0.08"/></proof>
......@@ -16,65 +16,65 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter remove.3" expl="3. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter remove.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter remove.5" expl="5. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter remove.6" expl="6. index in array bounds">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter remove.7" expl="7. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="WP_parameter remove.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter remove.9" expl="9. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove.10" expl="10. type invariant">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.12" steps="34"/></proof>
<proof prover="3"><result status="valid" time="0.12" steps="34"/></proof>
</goal>
<goal name="WP_parameter remove.12" expl="12. postcondition">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter put_back" expl="VC for put_back" expanded="true">
<goal name="WP_parameter put_back" expl="VC for put_back">
<transf name="split_goal_wp">
<goal name="WP_parameter put_back.1" expl="1. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter put_back.2" expl="2. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter put_back.3" expl="3. type invariant">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter put_back.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter put_back.5" expl="5. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="WP_parameter put_back.6" expl="6. type invariant">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter put_back.7" expl="7. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter put_back.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.17" steps="35"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="35"/></proof>
</goal>
<goal name="WP_parameter put_back.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.80"/></proof>
<proof prover="2"><result status="valid" time="0.54"/></proof>
</goal>
</transf>
</goal>
......
......@@ -14,8 +14,8 @@ theory Seq
type seq 'a
(** if ['a] is an infinite type, then [set 'a] is infinite *)
meta "material_type_arg" type seq, 0
(** [seq 'a] is an infinite type *)
meta "infinite_type" type seq
(** length *)
......
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