Skip to content

GitLab

Commit 6b219bee authored by MARCHE Claude's avatar MARCHE Claude
Browse files

session update

parent 6815352e
Hide whitespace changes
Inline Side-by-side
examples/programs/gcd/why3session.xml
View file @ 6b219bee
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./programs/gcd/why3session.xml">
name="programs/gcd/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -24,19 +24,19 @@
expanded="false">
<theory
name="WP EuclideanAlgorithm"
locfile="./programs/gcd/../gcd.mlw"
locfile="programs/gcd/../gcd.mlw"
loclnum="4" loccnumb="7" loccnume="25"
verified="true"
expanded="true">
<goal
name="WP_parameter gcd"
locfile="./programs/gcd/../gcd.mlw"
locfile="programs/gcd/../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="parameter gcd"
sum="bb383fa960a8a7dc480acf5a9477f9b0"
sum="d8c4bc6f48381e84e04969b311efba00"
proved="true"
expanded="true"
shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix >=V1c0Aainfix >=V0c0FF">
shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Aainfix &lt;amodV0V1V1Aainfix &lt;=c0V1Iainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<transf
......@@ -45,18 +45,19 @@
expanded="true">
<goal
name="WP_parameter gcd.1"
locfile="./programs/gcd/../gcd.mlw"
locfile="programs/gcd/../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="normal postcondition"
sum="fc52e4209870ce75f5a9e440c7653a9f"
sum="d5f9c6d980a45600967f0cbd467afea2"
proved="true"
expanded="true"
shape="ainfix =V0agcdV0V1Iainfix =V1c0Iainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =V0agcdV0V1Iainfix =V1c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="3"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......@@ -64,13 +65,15 @@
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="2"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -78,18 +81,19 @@
</goal>
<goal
name="WP_parameter gcd.2"
locfile="./programs/gcd/../gcd.mlw"
locfile="programs/gcd/../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="precondition"
sum="8eb8ac0ff31fff39bc1fa9ff6822b257"
sum="ba5000dd7ab2a92ea5138c6f3d3950cd"
proved="true"
expanded="true"
shape="ainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Aainfix &lt;amodV0V1V1Aainfix &lt;=c0V1Iainfix =V1c0NIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="3"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......@@ -97,6 +101,7 @@
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -104,29 +109,31 @@
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.3"
locfile="./programs/gcd/../gcd.mlw"
locfile="programs/gcd/../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="normal postcondition"
sum="b7f5a11a80c1407e1fce1c1292785688"
sum="92c5d9f0fadcfcaedc9ffd9ccc7e8bd2"
proved="true"
expanded="true"
shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Aainfix &lt;amodV0V1V1Aainfix &lt;=c0V1Iainfix =V1c0NIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="2"
timelimit="10"
memlimit="0"
edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
</transf>
......
examples/programs/gcd_bezout/why3session.xml
View file @ 6b219bee
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./programs/gcd_bezout/why3session.xml">
name="programs/gcd_bezout/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -20,19 +20,19 @@
expanded="false">
<theory
name="WP GcdBezout"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="4" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="WP_parameter gcd"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="e4a2c5a5d4862daa55c1df00cc730951"
sum="b902608a56a4e87fdc894d9ba0c73395"
proved="true"
expanded="true"
shape="iainfix >V6c0ainfix <V9V6Aainfix <=c0V6Aainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6Fainfix =ainfix +ainfix *V14V0ainfix *V15V1V7EAainfix =V7agcdV0V1Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFAainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF">
shape="iainfix &gt;V6c0ainfix &lt;V9V6Aainfix &lt;=c0V6Aainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix &gt;=V9c0Aainfix &gt;=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6Fainfix =ainfix +ainfix *V14V0ainfix *V15V1V7EAainfix =V7agcdV0V1Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFAainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix &gt;=V1c0Aainfix &gt;=V0c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<transf
......@@ -41,32 +41,33 @@
expanded="true">
<goal
name="WP_parameter gcd.1"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="loop invariant init"
sum="79bb0c1f17a0a39178611ac5f1bc2262"
sum="5235bb68096addff97b99a495f3e92d2"
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix &gt;=V1c0Aainfix &gt;=V0c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.2"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="loop invariant preservation"
sum="6514f3426b86561d591f90dc6738aa3c"
sum="4df161d8c53568375be7e7dea9b2e199"
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix &gt;=V9c0Aainfix &gt;=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix &gt;V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<transf
......@@ -75,18 +76,19 @@
expanded="true">
<goal
name="WP_parameter gcd.2.1"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="0689068fda4b9499a26d8c19e952f93a"
sum="8e1cc1854f856381dab4fbfec4cb13da"
proved="true"
expanded="true"
shape="ainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix &gt;=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix &gt;V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......@@ -94,6 +96,7 @@
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......@@ -101,18 +104,19 @@
</goal>
<goal
name="WP_parameter gcd.2.2"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="5785593adcf06f7a2e2b61ccc4a4606b"
sum="f3b43220fc3e43850f16ee605e8c9b9e"
proved="true"
expanded="true"
shape="ainfix >=V9c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix &gt;=V9c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix &gt;V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......@@ -120,71 +124,76 @@
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.2.3"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="2123ec7126e7bb899606e5e84c3383c1"
sum="41636bf746068fabd34cb9461499074e"
proved="true"
expanded="true"
shape="ainfix =agcdV8V9agcdV0V1Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =agcdV8V9agcdV0V1Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix &gt;V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="2"
timelimit="10"
memlimit="0"
edited="gcd_bezout_WP_GcdBezout_WP_parameter_gcd_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.67"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.2.4"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="8aeec7a08671ff3b0229de6143467b18"
sum="4e322cbd78095100c0f168c5f10a205f"
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix &gt;V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.2.5"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="18fdf83b194828ef616e9676cfafea02"
sum="60d9313c34d31942e589a4a7fc402647"
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix &gt;V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......@@ -194,32 +203,33 @@
</goal>
<goal
name="WP_parameter gcd.3"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="loop variant decreases"
sum="bd15228e8313441e41d4cb4edbfe28e7"
sum="8d608c4a92ece9ff4dfbf0152062a33e"
proved="true"
expanded="true"
shape="ainfix <V9V6Aainfix <=c0V6Iainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix &lt;V9V6Aainfix &lt;=c0V6Iainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix &gt;=V9c0Aainfix &gt;=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix &gt;V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.4"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="normal postcondition"
sum="49fdf592e8c24d6b4165b01938d10969"
sum="4f09b17bc934dd036d55738af2d4c440"
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EAainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EAainfix =V7agcdV0V1Iainfix &gt;V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<transf
......@@ -228,37 +238,39 @@
expanded="true">
<goal
name="WP_parameter gcd.4.1"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="099f9a5ebd3154d28dcdfb6f4a80c753"
sum="6d12895b4aaa206efd052ce361bc46b8"
proved="true"
expanded="true"
shape="ainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =V7agcdV0V1Iainfix &gt;V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.4.2"
locfile="./programs/gcd_bezout/../gcd_bezout.mlw"
locfile="programs/gcd_bezout/../gcd_bezout.mlw"
loclnum="11" loccnumb="6" loccnume="9"
expl="parameter gcd"
sum="b29847646f3bf08e778e5f844f0a74b6"
sum="967cba487e0da4fbd8b770c5a29af08a"
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EIainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EIainfix &gt;V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix &gt;=V6c0Aainfix &gt;=V7c0FFFFFFIainfix &gt;=V1c0Aainfix &gt;=V0c0FF">
<label
name="expl:parameter gcd"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......
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