Skip to content

GitLab

Commit 3ff9d439 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

update sessions

parent 04e9f107
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1401 additions and 1362 deletions
examples/programs/algo63/why3session.xml
View file @ 3ff9d439
This diff is collapsed.
examples/programs/algo64/why3session.xml
View file @ 3ff9d439
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/algo64/why3session.xml" shape_version="2">
<prover
......@@ -72,7 +72,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -92,7 +92,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -100,10 +100,10 @@
locfile="programs/algo64/../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="assertion"
sum="7e618d28b8912fce23207f86b654a106"
sum="e38f0c946373a1995809ee5c0c466dfe"
proved="true"
expanded="false"
shape="apermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
shape="apermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quicksort"/>
<proof
......@@ -112,7 +112,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -120,10 +120,10 @@
locfile="programs/algo64/../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="variant decreases"
sum="be29356540c6806e6793ab759cce41d4"
sum="1db9ef0fd17e657063f61aac9148fd8d"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
shape="ainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quicksort"/>
<proof
......@@ -140,10 +140,10 @@
locfile="programs/algo64/../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="precondition"
sum="ee3a6dea1e173389254b0f12c67064aa"
sum="3230e43afcedfba2f5761b2bd5dd4b93"
proved="true"
expanded="false"
shape="ainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
shape="ainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quicksort"/>
<proof
......@@ -160,10 +160,10 @@
locfile="programs/algo64/../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="assertion"
sum="33861baf2bddfa86de75f63fd85356d0"
sum="af85ec1817492490de4d45b7179a2866"
proved="true"
expanded="false"
shape="apermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
shape="apermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quicksort"/>
<proof
......@@ -180,10 +180,10 @@
locfile="programs/algo64/../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="normal postcondition"
sum="c3d9ffbd7445622e998ad133a20449a6"
sum="fb860a740a4ce478030b7ab12d6a50d3"
proved="true"
expanded="true"
shape="asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
shape="asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quicksort"/>
<transf
......@@ -195,10 +195,10 @@
locfile="programs/algo64/../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="parameter quicksort"
sum="36ecfbb78649dd92131e1eb53d740a9a"
sum="4b8b04d1cf923b7889d14fdb2530f478"
proved="true"
expanded="false"
shape="apermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
shape="apermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quicksort"/>
<proof
......@@ -215,10 +215,10 @@
locfile="programs/algo64/../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="parameter quicksort"
sum="561995d79c5365de26ec6c5c4e18bb7f"
sum="ffb31b94e3cf8ede84148c2b2743d6a8"
proved="true"
expanded="true"
shape="asorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
shape="asorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quicksort"/>
<proof
......@@ -227,7 +227,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="4.14"/>
<result status="valid" time="17.93"/>
</proof>
</goal>
</transf>
......
examples/programs/algo65/why3session.xml
View file @ 3ff9d439
This diff is collapsed.
examples/programs/arm/why3session.xml
View file @ 3ff9d439
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="examples/programs/arm/why3session.xml">
name="examples/programs/arm/why3session.xml" shape_version="2">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.2pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="z3"
name="Z3 smtv1"
version="2.2"/>
id="1"
name="Z3"
version="3.2"/>
<file
name="../arm.mlw"
verified="false"
expanded="true">
<theory
name="WP M"
name="M"
locfile="examples/programs/arm/../arm.mlw"
loclnum="4" loccnumb="7" loccnume="8"
verified="false"
expanded="true">
<goal
name="WP_parameter insertion_sort"
locfile="examples/programs/arm/../arm.mlw"
loclnum="17" loccnumb="6" loccnume="20"
expl="parameter insertion_sort"
sum="e4d2f23cb15a5aabb590bc249287e0dc"
sum="dbb9dfe3f395d80dedbd7726d136285d"
proved="false"
expanded="false"
shape="Lamk arrayV0V3Lamk arrayV0V8iainfix <=V5c10Lamk arrayV0V13iainfix <agetV13V11agetV13ainfix -V11c1ainfix <V18V11Aainfix <=c0V11Aainfix <=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix <=V18V5Aainfix <=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V15ainfix +V12c1Fainfix <ainfix -c10V19ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix <=V19c11Aainfix <=c2V19Iainfix =V19ainfix +V5c1FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11FFFAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V6c45Aainfix =V7c9Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5FFFFAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4FFFF">
shape="iainfix &lt;=V5c10iainfix &lt;agetV13V11agetV13ainfix -V11c1ainfix &lt;V18V11Aainfix &lt;=c0V11Aainfix &lt;=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix &lt;=V18V5Aainfix &lt;=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11FAainfix &lt;ainfix -V11c1V0Aainfix &lt;=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;ainfix -V11c1V0Aainfix &lt;=c0ainfix -V11c1Aainfix &lt;V11V0Aainfix &lt;=c0V11Iainfix =V15ainfix +V12c1Fainfix &lt;ainfix -c10V19ainfix -c10V5Aainfix &lt;=c0ainfix -c10V5Aainfix &lt;=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix &lt;=V19c11Aainfix &lt;=c2V19Iainfix =V19ainfix +V5c1FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;ainfix -V11c1V0Aainfix &lt;=c0ainfix -V11c1Iainfix &lt;=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix &lt;=V11V5Aainfix &lt;=c1V11Lamk arrayV0V13FAainfix &lt;=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix &lt;=V5V5Aainfix &lt;=c1V5Iainfix =V10ainfix +V7c1Fainfix &lt;=V6c45Aainfix =V7c9Iainfix &lt;=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix &lt;=V5c11Aainfix &lt;=c2V5Lamk arrayV0V8FAainfix &lt;=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix &lt;=c2c11Aainfix &lt;=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Lamk arrayV0V3FF">
<label
name="expl:parameter insertion_sort"/>
</goal>
</theory>
<theory
name="WP ARM"
name="ARM"
locfile="examples/programs/arm/../arm.mlw"
loclnum="42" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
</theory>
<theory
name="WP InsertionSortExample"
name="InsertionSortExample"
locfile="examples/programs/arm/../arm.mlw"
loclnum="100" loccnumb="7" loccnume="27"
verified="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter path_init_l2"
locfile="examples/programs/arm/../arm.mlw"
loclnum="122" loccnumb="6" loccnume="18"
expl="normal postcondition"
sum="c2c5ea2cbb588e6cd95f3653c4f1f8fb"
sum="795f8de35a06a3c2af46ce51dec5f462"
proved="true"
expanded="false"
shape="ainv_l2V5V0V2Iainfix =V5amixfix [<-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0FF">
expanded="true"
shape="ainv_l2V5V0V2Iainfix =V5amixfix [&lt;-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F">
<label
name="expl:parameter path_init_l2"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter path_l2_exit"
locfile="examples/programs/arm/../arm.mlw"
loclnum="129" loccnumb="6" loccnume="18"
expl="normal postcondition"
sum="aad12da07e3d91a9a0721b583a6decc3"
sum="15ab5996d34e86896c649b5e2e7646ff"
proved="true"
expanded="false"
shape="ainfix =V0c9Iainfix =V4aTrueNIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1FFF">
expanded="true"
shape="ainfix =V0c9Iainfix =V4aFalseIainfix &lt;=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F">
<label
name="expl:parameter path_l2_exit"/>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
examples/programs/fibonacci/fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v
View file @ 3ff9d439
......@@ -67,6 +67,9 @@ Axiom Power_0 : forall (x:t), ((power x 0%Z) = (mk_t 1%Z 0%Z 0%Z 1%Z)).
Axiom Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
(n + 1%Z)%Z) = (mult x (power x n))).
Axiom Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x n) = (mult x
(power x (n - 1%Z)%Z))).
Axiom Power_1 : forall (x:t), ((power x 1%Z) = x).
Axiom Power_sum : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
......@@ -78,11 +81,9 @@ Axiom Power_mult : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
Axiom Power_mult2 : forall (x:t) (y:t) (n:Z), (0%Z <= n)%Z -> ((power (mult x
y) n) = (mult (power x n) (power y n))).
(* Why3 goal *)
Theorem WP_parameter_logfib : forall (n:Z), (0%Z <= n)%Z -> ((~ (n = 0%Z)) ->
((((0%Z <= n)%Z /\ ((int.EuclideanDivision.div n 2%Z) < n)%Z) /\
(0%Z <= (int.EuclideanDivision.div n 2%Z))%Z) -> forall (result:Z)
((0%Z <= (int.EuclideanDivision.div n 2%Z))%Z -> forall (result:Z)
(result1:Z), ((power (mk_t 1%Z 1%Z 1%Z 0%Z) (int.EuclideanDivision.div n
2%Z)) = (mk_t (result + result1)%Z result1 result1 result)) ->
((((int.EuclideanDivision.mod1 n 2%Z) = 0%Z) -> let a :=
......@@ -102,7 +103,7 @@ intuition.
rewrite H4 in H3.
rewrite H3.
replace (2 * div n 2 + 0)%Z with (div n 2 + div n 2)%Z by omega.
rewrite Power_sum by exact H5.
rewrite Power_sum by exact H1.
rewrite H2; simpl.
unfold mult; simpl.
apply f_equal4; ring.
......@@ -115,7 +116,7 @@ rewrite h' in H3.
rewrite H3.
replace (2 * div n 2 + 1)%Z with ((div n 2 + div n 2) + 1)%Z by omega.
rewrite Power_s.
rewrite Power_sum by exact H5.
rewrite Power_sum by exact H1.
rewrite H2; simpl.
unfold mult at 2; simpl.
unfold mult.
......
examples/programs/fibonacci/why3session.xml
View file @ 3ff9d439
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/fibonacci/why3session.xml" shape_version="2">
name="examples/programs/fibonacci/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -36,7 +36,7 @@
expanded="true">
<theory
name="Fibonacci"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="2" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
......@@ -45,13 +45,13 @@
</theory>
<theory
name="FibonacciTest"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="14" loccnumb="7" loccnume="20"
verified="true"
expanded="false">
<goal
name="isfib_2_1"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="18" loccnumb="8" loccnume="17"
sum="d9eabf8d7568cdd6e09c64f34668cca8"
proved="true"
......@@ -68,7 +68,7 @@
</goal>
<goal
name="isfib_6_8"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="19" loccnumb="8" loccnume="17"
sum="9d93314ed80fc04190c1765d6323461d"
proved="true"
......@@ -85,7 +85,7 @@
</goal>
<goal
name="not_isfib_2_2"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="21" loccnumb="8" loccnume="21"
sum="a40d1bc22627a0babb88a4481a9541a5"
proved="true"
......@@ -129,19 +129,19 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
<theory
name="FibonacciLinear"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="25" loccnumb="7" loccnume="22"
verified="true"
expanded="false">
<goal
name="WP_parameter fib"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="31" loccnumb="6" loccnume="9"
expl="parameter fib"
sum="350a514a1ca03b5d98dc329a7b5c6f2d"
......@@ -156,13 +156,13 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="Mat22"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="46" loccnumb="7" loccnume="12"
verified="true"
expanded="true">
......@@ -171,13 +171,13 @@
</theory>
<theory
name="FibonacciLogarithmic"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="68" loccnumb="7" loccnume="27"
verified="true"
expanded="true">
<goal
name="WP_parameter logfib"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="parameter logfib"
sum="be18b57a378e8f58833c62cc4852ff5c"
......@@ -192,7 +192,7 @@
expanded="true">
<goal
name="WP_parameter logfib.1"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="normal postcondition"
sum="54ff9f48d80a0d661479ac9f4110b022"
......@@ -207,7 +207,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -215,7 +215,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -223,7 +223,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -236,7 +236,7 @@
</goal>
<goal
name="WP_parameter logfib.2"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="variant decreases"
sum="024ee6b3b1eb5f5cb113823603c892cf"
......@@ -251,12 +251,12 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter logfib.3"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="precondition"
sum="f98d6f543cdf82e62fc44c18db5e7230"
......@@ -284,13 +284,13 @@
</goal>
<goal
name="WP_parameter logfib.4"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="normal postcondition"
sum="807ed294a6590eb6e850dbd8ab7ffd80"
sum="4124e6c67675b5e5aa3e4feca51111a1"
proved="true"
expanded="false"
shape="iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FIainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
expanded="true"
shape="iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FIainfix &gt;=adivV0c2c0Iainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
<proof
......@@ -300,14 +300,14 @@
edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.60"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="fib_m"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="105" loccnumb="8" loccnume="13"
sum="a63b2ce2736615025314f4148f50ebfc"
proved="true"
......@@ -320,12 +320,12 @@
edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.54"/>
</proof>
</goal>
<goal
name="WP_parameter fibo"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="109" loccnumb="6" loccnume="10"
expl="parameter fibo"
sum="c3f07c9fe36f4699cf6d127472aa26e7"
......
examples/programs/gcd/why3session.xml
View file @ 3ff9d439
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/gcd/why3session.xml" shape_version="2">
<prover
......@@ -64,7 +64,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -72,7 +72,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -100,7 +100,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.20"/>
<result status="valid" time="0.21"/>
</proof>
<proof
prover="2"
......@@ -128,7 +128,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -136,7 +136,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -144,7 +144,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -152,10 +152,10 @@
locfile="programs/gcd/../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="normal postcondition"
sum="8c935721b94f1ac90fc16aa90cb62bad"
sum="10b988e8ea93877fe03afeaeedba84b1"
proved="true"
expanded="true"
shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Aainfix &lt;amodV0V1V1Aainfix &lt;=c0V1Iainfix =V1c0NIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Iainfix =V1c0NIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:parameter gcd"/>
<proof
......@@ -165,7 +165,7 @@
edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.59"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
</transf>
......
examples/programs/insertion_sort_list/why3session.xml
View file @ 3ff9d439
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/insertion_sort_list/why3session.xml" shape_version="2">
<prover
......@@ -28,7 +28,7 @@
name="WP_parameter insert"