Commit 04ff49e1 authored by MARCHE Claude's avatar MARCHE Claude

updated obsolete sessions

parent 6d133aba
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="32" loccnumb="8" loccnume="11" loclnum="32" loccnumb="8" loccnume="11"
expl="VC for sum" expl="VC for sum"
sum="72c83e84b67c41630bc8294cd68c64f5" sum="0a492f8ad504c050cdce87f294c7e321"
proved="true" proved="true"
expanded="true" expanded="true"
shape="Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F"> shape="Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F">
...@@ -71,7 +71,7 @@ ...@@ -71,7 +71,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="45" loccnumb="4" loccnume="8" loclnum="45" loccnumb="4" loccnume="8"
expl="VC for main" expl="VC for main"
sum="ecbcde4cd071b18e708a736b4cdd0a7a" sum="e4ee17c3f0db6f44050cfe5e902ce0cf"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil"> shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil">
...@@ -106,7 +106,7 @@ ...@@ -106,7 +106,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="64" loccnumb="4" loccnume="7" loclnum="64" loccnumb="4" loccnume="7"
expl="VC for sum" expl="VC for sum"
sum="83604e216310af600dfb7ba405d37f6f" sum="0f9b53b209abc77940c4947079bdeb93"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F"> shape="ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
...@@ -134,7 +134,7 @@ ...@@ -134,7 +134,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="88" loccnumb="4" loccnume="8" loclnum="88" loccnumb="4" loccnume="8"
expl="VC for main" expl="VC for main"
sum="9e8d6db4780d4242bc778a1123f8969f" sum="bd44a1ba46c51b25c11a2cfdaf1b3abd"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil"> shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil">
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
locfile="../assigning_meanings_to_programs.mlw" locfile="../assigning_meanings_to_programs.mlw"
loclnum="12" loccnumb="6" loccnume="9" loclnum="12" loccnumb="6" loccnume="9"
expl="VC for sum" expl="VC for sum"
sum="a22a8b12b1c0d38016349831b652911b" sum="329d3acbda193f226c9e300474bf832a"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix =V3asumV1c1ainfix +V2c1ainfix <ainfix -V2V6ainfix -V2V4Aainfix <=c0ainfix -V2V4Aainfix =V5asumV1c1V6Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV1V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V2Iainfix =V3asumV1c1V4Aainfix <=V4ainfix +V2c1Aainfix <=c1V4FAainfix =c0asumV1c1c1Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Aainfix <=c0V2Aainfix <=c0V0F"> shape="iainfix =V3asumV1c1ainfix +V2c1ainfix <ainfix -V2V6ainfix -V2V4Aainfix <=c0ainfix -V2V4Aainfix =V5asumV1c1V6Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV1V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V2Iainfix =V3asumV1c1V4Aainfix <=V4ainfix +V2c1Aainfix <=c1V4FAainfix =c0asumV1c1c1Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Aainfix <=c0V2Aainfix <=c0V0F">
...@@ -51,7 +51,7 @@ ...@@ -51,7 +51,7 @@
locfile="../assigning_meanings_to_programs.mlw" locfile="../assigning_meanings_to_programs.mlw"
loclnum="38" loccnumb="6" loccnume="14" loclnum="38" loccnumb="6" loccnume="14"
expl="VC for division" expl="VC for division"
sum="f5a622ea8cf386291b709e9e4e6ad22a" sum="188bd14860a30ee027c058f8c34ad87a"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix >=V2V1Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0F"> shape="iainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix >=V2V1Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0F">
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
name="closest" name="closest"
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="34" loccnumb="8" loccnume="15" loclnum="34" loccnumb="8" loccnume="15"
sum="c18e4a733a845b9d1202d0b801bbf0f3" sum="95d8e3e83400477156b0c6fbd6ebe59e"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix <=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix <=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0F"> shape="ainfix <=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix <=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0F">
...@@ -46,7 +46,7 @@ ...@@ -46,7 +46,7 @@
edited="bresenham_M_closest_1.v" edited="bresenham_M_closest_1.v"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="3.74"/> <result status="valid" time="1.29"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -54,7 +54,7 @@ ...@@ -54,7 +54,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="VC for bresenham" expl="VC for bresenham"
sum="9b8128bb23b676133822da0cac2fea53" sum="7ba5580c4640dde414e2e5c479466406"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix &lt;=V6ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix &lt;V1c0AabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFAainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2"> shape="iainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix &lt;=V6ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix &lt;V1c0AabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFAainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2">
...@@ -69,7 +69,7 @@ ...@@ -69,7 +69,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="1. loop invariant init" expl="1. loop invariant init"
sum="818d60808053e43e7be4da19c039bf40" sum="73bac718d188f399d95c94526ff00d45"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2"> shape="loop invariant initainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2">
...@@ -105,7 +105,7 @@ ...@@ -105,7 +105,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="2. loop invariant init" expl="2. loop invariant init"
sum="4ed4f3c9453360f984689a439a94d03a" sum="d3ff8f58676f65292f348f1e01ad13c6"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Iainfix &lt;=c0V0Lax2"> shape="loop invariant initainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Iainfix &lt;=c0V0Lax2">
...@@ -125,7 +125,7 @@ ...@@ -125,7 +125,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="3. assertion" expl="3. assertion"
sum="fcbcee9000353217b3dbca58d7cc9146" sum="145816b0641871a72f5fd04fc38bd8af"
proved="true" proved="true"
expanded="true" expanded="true"
shape="assertionabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="assertionabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
...@@ -137,7 +137,7 @@ ...@@ -137,7 +137,7 @@
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="6.17"/> <result status="valid" time="1.86"/>
</proof> </proof>
<proof <proof
prover="1" prover="1"
...@@ -145,7 +145,7 @@ ...@@ -145,7 +145,7 @@
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="6.86"/> <result status="valid" time="1.80"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -153,7 +153,7 @@ ...@@ -153,7 +153,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="4. loop invariant preservation" expl="4. loop invariant preservation"
sum="0926f96b84b6aebff66f2379e7c0e76e" sum="0c464430697f406b20cf1199bd5adfb9"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V4ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix =V4ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
...@@ -189,7 +189,7 @@ ...@@ -189,7 +189,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="5. loop invariant preservation" expl="5. loop invariant preservation"
sum="46f21c9ec9008592af315031d0658467" sum="4b9a313a3ab1ccca4f6b19eb2c6d673f"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix &lt;=V4ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V4Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix &lt;=V4ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V4Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
...@@ -209,7 +209,7 @@ ...@@ -209,7 +209,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="6. loop invariant preservation" expl="6. loop invariant preservation"
sum="effb2332ccb437bc6e30129ae779efb0" sum="8c9dfb21ea36fe4493a3fe323019ebd6"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
...@@ -229,7 +229,7 @@ ...@@ -229,7 +229,7 @@
memlimit="0" memlimit="0"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.95"/> <result status="valid" time="0.28"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -237,7 +237,7 @@ ...@@ -237,7 +237,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="7. loop invariant preservation" expl="7. loop invariant preservation"
sum="60e316bbceaf72ebb290a196c9b2d99f" sum="c4eeab8e74f4cc05b9c39bab40e5a4b7"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
......
...@@ -27,7 +27,7 @@ ...@@ -27,7 +27,7 @@
locfile="../13375.mlw" locfile="../13375.mlw"
loclnum="51" loccnumb="5" loccnume="12" loclnum="51" loccnumb="5" loccnume="12"
expl="VC for to_int_" expl="VC for to_int_"
sum="e6a711bfdd6682b19fabf8bf80de62d2" sum="32f921fac01c5c8809e2cb26c095e80a"
proved="true" proved="true"
expanded="true" expanded="true"
shape="t"> shape="t">
......
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
locfile="../13853.mlw" locfile="../13853.mlw"
loclnum="16" loccnumb="8" loccnume="9" loclnum="16" loccnumb="8" loccnume="9"
expl="VC for f" expl="VC for f"
sum="fdfdcd8a1f137c078f0abe9250e1cce9" sum="b02952dbc728d0247c4fc708f2e40d93"
proved="true" proved="true"
expanded="true" expanded="true"
shape="t"> shape="t">
...@@ -40,7 +40,7 @@ ...@@ -40,7 +40,7 @@
locfile="../13853.mlw" locfile="../13853.mlw"
loclnum="17" loccnumb="8" loccnume="9" loclnum="17" loccnumb="8" loccnume="9"
expl="VC for g" expl="VC for g"
sum="2025d70e832acc7e1ff2583948c31de9" sum="1457d9f96317c678855684b7f490c772"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix &lt;c0c1Aainfix &lt;=c0c1"> shape="ainfix &lt;c0c1Aainfix &lt;=c0c1">
......
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="VC for routine" expl="VC for routine"
sum="9028bb052f853665b3d323d2b19dfc50" sum="b6b5481cb51b7e0c70ff9af6915ef113"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix =V1afactV0iainfix &lt;ainfix -V0V5ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Aainfix =V4afactV5Aainfix &lt;=V5V0Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1Fainfix &lt;ainfix -V2V7ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix =V6ainfix *V7afactV2Aainfix &lt;=V7ainfix +V2c1Aainfix &lt;=c1V7Iainfix =V7ainfix +V3c1FIainfix =V6ainfix +V4V1Fainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FAainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1ainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FAainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F"> shape="iainfix =V1afactV0iainfix &lt;ainfix -V0V5ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Aainfix =V4afactV5Aainfix &lt;=V5V0Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1Fainfix &lt;ainfix -V2V7ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix =V6ainfix *V7afactV2Aainfix &lt;=V7ainfix +V2c1Aainfix &lt;=c1V7Iainfix =V7ainfix +V3c1FIainfix =V6ainfix +V4V1Fainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FAainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1ainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FAainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
...@@ -39,7 +39,7 @@ ...@@ -39,7 +39,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="1. loop invariant init" expl="1. loop invariant init"
sum="5e85633930721ccde15b77bd37db8970" sum="0eb61307b91c2331318ee93f9effac3c"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F"> shape="loop invariant initainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
...@@ -59,7 +59,7 @@ ...@@ -59,7 +59,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="2. loop invariant init" expl="2. loop invariant init"
sum="fdb154b730c0cafc3232df24a5cdaa88" sum="17cdb36ee2341f2279e0cf83995fdb58"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1Iainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F"> shape="loop invariant initainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1Iainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
...@@ -79,7 +79,7 @@ ...@@ -79,7 +79,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="3. loop invariant preservation" expl="3. loop invariant preservation"
sum="625fc39700faa574f948d4e3620ac349" sum="1ace46d516a0fdf573b4e9bb4b8a4e0c"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V5ainfix *V6afactV2Aainfix &lt;=V6ainfix +V2c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F"> shape="loop invariant preservationainfix =V5ainfix *V6afactV2Aainfix &lt;=V6ainfix +V2c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
...@@ -99,7 +99,7 @@ ...@@ -99,7 +99,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="4. loop variant decrease" expl="4. loop variant decrease"
sum="bd77cce67743829f073a59e157745762" sum="1578eeea58be86a10c85e40060cec867"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop variant decreaseainfix &lt;ainfix -V2V6ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F"> shape="loop variant decreaseainfix &lt;ainfix -V2V6ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
...@@ -119,7 +119,7 @@ ...@@ -119,7 +119,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="5. loop invariant preservation" expl="5. loop invariant preservation"
sum="a60c94b84bb74652d744241ab7559be6" sum="eefe4b3483bb694f5ca92a7722cbd546"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V4afactV5Aainfix &lt;=V5V0Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1FINainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F"> shape="loop invariant preservationainfix =V4afactV5Aainfix &lt;=V5V0Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1FINainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
...@@ -139,7 +139,7 @@ ...@@ -139,7 +139,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="6. loop variant decrease" expl="6. loop variant decrease"
sum="6ea25727fb4618dcc0d3b7ab9333f3fd" sum="7a85e21f66f49405053c48f4d8c159e3"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop variant decreaseainfix &lt;ainfix -V0V5ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Iainfix =V5ainfix +V2c1FINainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F"> shape="loop variant decreaseainfix &lt;ainfix -V0V5ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Iainfix =V5ainfix +V2c1FINainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
...@@ -159,7 +159,7 @@ ...@@ -159,7 +159,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="7. postcondition" expl="7. postcondition"
sum="54ac74a0f40458aca9c976064b73b1bb" sum="c8d4f9bc758f1be2b89ead1120ac33dc"
proved="true" proved="true"
expanded="true" expanded="true"
shape="postconditionainfix =V1afactV0INainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F"> shape="postconditionainfix =V1afactV0INainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
...@@ -181,7 +181,7 @@ ...@@ -181,7 +181,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="VC for routine2" expl="VC for routine2"
sum="8ad714dc13aab5e8d912904330e01693" sum="cd3b8e0513993bb30efb41ed23ef34d4"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V2afactV0Iainfix =V2afactainfix +V1c1Aainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3Aainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix &lt;=V5V3Aainfix &lt;=c1V5FFAainfix =V2ainfix *c1afactV3Iainfix &lt;=c1V3Aainfix =V2afactainfix +V3c1Iainfix &gt;c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFAainfix =c1afactc0Iainfix &lt;=c0V1Aainfix =c1afactV0Iainfix &gt;c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="ainfix =V2afactV0Iainfix =V2afactainfix +V1c1Aainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3Aainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix &lt;=V5V3Aainfix &lt;=c1V5FFAainfix =V2ainfix *c1afactV3Iainfix &lt;=c1V3Aainfix =V2afactainfix +V3c1Iainfix &gt;c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFAainfix =c1afactc0Iainfix &lt;=c0V1Aainfix =c1afactV0Iainfix &gt;c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
...@@ -196,7 +196,7 @@ ...@@ -196,7 +196,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="1. postcondition" expl="1. postcondition"
sum="db19aa1c1bc3d5cf1ca85d08e394718c" sum="f18d3e5252e4c202abc17515531067ba"
proved="true" proved="true"
expanded="true" expanded="true"
shape="postconditionainfix =c1afactV0Iainfix &gt;c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="postconditionainfix =c1afactV0Iainfix &gt;c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
...@@ -216,7 +216,7 @@ ...@@ -216,7 +216,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="2. loop invariant init" expl="2. loop invariant init"
sum="a1cd7023e9565fb9ab8956edfe0522b5" sum="309ddfa2c36dc1b8fde6e7e1721c83d2"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =c1afactc0Iainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="loop invariant initainfix =c1afactc0Iainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
...@@ -236,7 +236,7 @@ ...@@ -236,7 +236,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="3. loop invariant preservation" expl="3. loop invariant preservation"
sum="5a7961404a2829ffe8b3732f7e0e2eaa" sum="4e9f02c291b0686631a49ed6e54e654f"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V2afactainfix +V3c1Iainfix &gt;c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="loop invariant preservationainfix =V2afactainfix +V3c1Iainfix &gt;c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
...@@ -256,7 +256,7 @@ ...@@ -256,7 +256,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="4. loop invariant init" expl="4. loop invariant init"
sum="08a955513f4e5a20d1159bb4e745e895" sum="32c64d5b033a385d1394b180d6b835aa"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =V2ainfix *c1afactV3Iainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="loop invariant initainfix =V2ainfix *c1afactV3Iainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
...@@ -276,7 +276,7 @@ ...@@ -276,7 +276,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="5. loop invariant preservation" expl="5. loop invariant preservation"
sum="cc3a49db2295ba19ad2c44b7ea7fe465" sum="f2da4444521bc9d9f94f1edd54098af3"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix &lt;=V5V3Aainfix &lt;=c1V5FFIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="loop invariant preservationainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix &lt;=V5V3Aainfix &lt;=c1V5FFIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
...@@ -296,7 +296,7 @@ ...@@ -296,7 +296,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="6. loop invariant preservation" expl="6. loop invariant preservation"
sum="bf809ddb0e91ab7ed09f3eeb86f8abd8" sum="e98222c8a5d88bb129eb443e02c662df"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3FIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="loop invariant preservationainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3FIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
...@@ -316,7 +316,7 @@ ...@@ -316,7 +316,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="7. postcondition" expl="7. postcondition"
sum="754f3053aa741a90e6fc0576da6088b0" sum="cec5ffbe4cde68dfe5c00dd13ee15719"
proved="true" proved="true"
expanded="true" expanded="true"
shape="postconditionainfix =V2afactV0Iainfix =V2afactainfix +V1c1FIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F"> shape="postconditionainfix =V2afactV0Iainfix =V2afactainfix +V1c1FIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="VC for division" expl="VC for division"
sum="d3b226e27a4e0acecc1bb23ea145e836" sum="17325b12d2a5ee97ba9722c3e954bfbb"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix &lt;V4V1Aainfix &lt;=c0V4Aainfix =ainfix +ainfix *V3V1V4V0Eainfix &lt;V6V2Aainfix &lt;=c0V2Aainfix &lt;=c0V6Aainfix =ainfix +ainfix *V5V1V6V0Iainfix =V6ainfix -V2V1FIainfix =V5ainfix +V3c1Fainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FAainfix &lt;=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix &lt;c0V1Aainfix &lt;=c0V0F"> shape="iainfix &lt;V4V1Aainfix &lt;=c0V4Aainfix =ainfix +ainfix *V3V1V4V0Eainfix &lt;V6V2Aainfix &lt;=c0V2Aainfix &lt;=c0V6Aainfix =ainfix +ainfix *V5V1V6V0Iainfix =V6ainfix -V2V1FIainfix =V5ainfix +V3c1Fainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FAainfix &lt;=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix &lt;c0V1Aainfix &lt;=c0V0F">
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="1. loop invariant init" expl="1. loop invariant init"
sum="52122f915616a89df4442b60734b4888" sum="23210e55ab366e193f6469f3dd8a7dc9"
proved="true" proved="true"
expanded="false" expanded="false"
shape="loop invariant initainfix &lt;=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix &lt;c0V1Aainfix &lt;=c0V0F"> shape="loop invariant initainfix &lt;=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix &lt;c0V1Aainfix &lt;=c0V0F">
...@@ -55,7 +55,7 @@ ...@@ -55,7 +55,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="2. loop invariant preservation" expl="2. loop invariant preservation"
sum="51eb50ac0b43bdf79bd3f69e91199fe9" sum="4f68a1a401e16e01cbc0584a2d13e5a8"
proved="true" proved="true"
expanded="false" expanded="false"
shape="loop invariant preservationainfix &lt;=c0V5Aainfix =ainfix +ainfix *V4V1V5V0Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix &lt;c0V1Aainfix &lt;=c0V0F"> shape="loop invariant preservationainfix &lt;=c0V5Aainfix =ainfix +ainfix *V4V1V5V0Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix &lt;c0V1Aainfix &lt;=c0V0F">
...@@ -75,7 +75,7 @@ ...@@ -75,7 +75,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="3. loop variant decrease" expl="3. loop variant decrease"
sum="70714135f606957803eaea8368919b09" sum="dbc2a65014dce06f159a71dd16dc7fff"
proved="true" proved="true"
expanded="false" expanded="false"
shape="loop variant decreaseainfix &lt;V5V2Aainfix &lt;=c0V2Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix &lt;c0V1Aainfix &lt;=c0V0F"> shape="loop variant decreaseainfix &lt;V5V2Aainfix &lt;=c0V2Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix &lt;c0V1Aainfix &lt;=c0V0F">
...@@ -95,7 +95,7 @@ ...@@ -95,7 +95,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="4. postcondition" expl="4. postcondition"
sum="8c80cc7291c854f28a428fb703341268" sum="0e720ad9c169791b83d053e9325c9ee3"
proved="true" proved="true"
expanded="true" expanded="true"
shape="postconditionainfix &lt;V4V1Aainfix &lt;=c0V4Aainfix =ainfix +ainfix *V3V1V4V0EINainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix &lt;c0V1Aainfix &lt;=c0V0F"> shape="postconditionainfix &lt;V4V1Aainfix &lt;=c0V4Aainfix =ainfix +ainfix *V3V1V4V0EINainfix &gt;=V2V1Iainfix &lt;=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix &lt;c0V1Aainfix &lt;=c0V0F">
......
This diff is collapsed.
...@@ -696,7 +696,7 @@ ...@@ -696,7 +696,7 @@
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"