Commit 4ca47a73 authored by MARCHE Claude's avatar MARCHE Claude

updated session again

parent e9e8cb08
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="programs/insertion_sort_list/why3session.xml">
name="examples/programs/insertion_sort_list/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -16,16 +16,16 @@
expanded="false">
<theory
name="WP M"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="4" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="WP_parameter insert"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="84e2aa9751598370fc4d9f6f9c5b4a40"
sum="8a1ed54c3f0c362fb144098bfd668b32"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix <=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1IasortedV1FF">
......@@ -38,10 +38,10 @@
expanded="true">
<goal
name="WP_parameter insert.1"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="4a69f68c5d460749f0ef438e15442acf"
sum="221159a13d4206a4460d1723c7561f5b"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVVtIasortedV1FF">
......@@ -53,15 +53,15 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter insert.2"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="ca1192523c9f6846cbe0519ed7977850"
sum="03780f98738f0a4d31b9f5cdafef018f"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV0V1AasortedaConsV0V1Iainfix <=V0V2IasortedV1FF">
......@@ -78,10 +78,10 @@
</goal>
<goal
name="WP_parameter insert.3"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="323ba14021e983aedaa70f389a6f9ca2"
sum="bd15c5616f0e48a457c665b7daeb5133"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
......@@ -93,15 +93,15 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter insert.4"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="3dd8034ce59793f25f60f2f400095552"
sum="17df99648aa521a75f2047df4cf0c6f0"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FIasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
......@@ -113,17 +113,17 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.18"/>
<result status="valid" time="0.11"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter insertion_sort"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="16d8a43872423232fe7bd6e35d3a5ba5"
sum="d28eefc56d379c5156175265bf010598"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FAasortedV3IapermutV2V3AasortedV3FAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -136,10 +136,10 @@
expanded="true">
<goal
name="WP_parameter insertion_sort.1"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="94c7e6b8ec2a0a739033d3bd222c577f"
sum="71173457dcb476b018a44d47d231ad49"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVtF">
......@@ -156,10 +156,10 @@
</goal>
<goal
name="WP_parameter insertion_sort.2"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="59f3bde7dbb179dd4ba4e0943bb955c7"
sum="17e9acde476c648319587d89cd36c1c8"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -183,10 +183,10 @@
</goal>
<goal
name="WP_parameter insertion_sort.3"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="01a3a1139967fc619194daefb574ad7e"
sum="80b0842e233ef20ca04bf6ed7b47e326"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVasortedV3IapermutV2V3AasortedV3FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -198,7 +198,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -210,10 +210,10 @@
</goal>
<goal
name="WP_parameter insertion_sort.4"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="0664d39ce85984eefbde659a0dd4e23a"
sum="70da74d76767b2269d36aef985b01798"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FIasortedV3IapermutV2V3AasortedV3FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -225,14 +225,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
......
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