Commit c4e7e01d authored by MARCHE Claude's avatar MARCHE Claude

update more sessions

parent eacd2b2c
......@@ -38,7 +38,7 @@
expl="VC for search"
sum="adfd7ec70c6b9a59e97dfc5050342eb1"
proved="true"
expanded="false"
expanded="true"
shape="Cano_zeroV1Aainfix =V0ainfix +V0alengthV1Oazero_atV1ainfix -V0V0Aainfix <V0ainfix +V0alengthV1Aainfix <=V0V0aNiliano_zeroV1Aainfix =V5ainfix +V0alengthV1Oazero_atV1ainfix -V5V0Aainfix <V5ainfix +V0alengthV1Aainfix <=V0V5Iano_zeroV3Aainfix =V5ainfix +V4alengthV3Oazero_atV3ainfix -V5V4Aainfix <V5ainfix +V4alengthV3Aainfix <=V4V5FACfaNilainfix =V6V3aConswVV1Lainfix +V0c1ano_zeroV1Aainfix =V0ainfix +V0alengthV1Oazero_atV1ainfix -V0V0Aainfix <V0ainfix +V0alengthV1Aainfix <=V0V0ainfix =V2c0aConsVVV1F">
<label
name="expl:VC for search"/>
......@@ -50,14 +50,6 @@
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="WP_parameter search_list"
......@@ -66,7 +58,7 @@
expl="VC for search_list"
sum="78076946b806713b7e99a024390f3156"
proved="true"
expanded="false"
expanded="true"
shape="ano_zeroV0Aainfix =V1alengthV0Oazero_atV0V1Aainfix &lt;V1alengthV0Aainfix &lt;=c0V1Iano_zeroV0Aainfix =V1ainfix +c0alengthV0Oazero_atV0ainfix -V1c0Aainfix &lt;V1ainfix +c0alengthV0Aainfix &lt;=c0V1FF">
<label
name="expl:VC for search_list"/>
......@@ -189,7 +181,7 @@
expl="1. loop invariant init"
sum="9a24e02441771c7ea14455352109e386"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant initNainfix =anthV1V0aSomec0Iainfix &lt;V1c0Aainfix &lt;=c0V1FAainfix =anthV2V0anthainfix +c0V2V0Iainfix &lt;=c0V2FAainfix =ainfix +c0alengthV0alengthV0Aainfix &lt;=c0c0F">
<label
name="expl:VC for search_loop"/>
......@@ -225,7 +217,7 @@
expl="2. precondition"
sum="776d12df23073d159058726e6eaac549"
proved="true"
expanded="true"
expanded="false"
shape="preconditionNainfix =V1aNilINainfix =V1aNilINainfix =anthV3V0aSomec0Iainfix &lt;V3V2Aainfix &lt;=c0V3FAainfix =anthV4V1anthainfix +V2V4V0Iainfix &lt;=c0V4FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -261,7 +253,7 @@
expl="3. precondition"
sum="e5f849731c68360a514c95372c9f6d84"
proved="true"
expanded="true"
expanded="false"
shape="preconditionNainfix =V1aNilIainfix =V4ainfix +V2c1FINainfix =V3c0ICfaNilainfix =V3V5aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV6V0aSomec0Iainfix &lt;V6V2Aainfix &lt;=c0V6FAainfix =anthV7V1anthainfix +V2V7V0Iainfix &lt;=c0V7FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -297,14 +289,14 @@
expl="4. loop invariant preservation"
sum="4e4f6766937ab37625f8692739d76880"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant preservationNainfix =anthV7V0aSomec0Iainfix &lt;V7V4Aainfix &lt;=c0V7FAainfix =anthV8V6anthainfix +V4V8V0Iainfix &lt;=c0V8FAainfix =ainfix +V4alengthV6alengthV0Aainfix &lt;=c0V4Iainfix =V6V5FICfaNilainfix =V5V9aConswVV1FINainfix =V1aNilIainfix =V4ainfix +V2c1FINainfix =V3c0ICfaNilainfix =V3V10aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV11V0aSomec0Iainfix &lt;V11V2Aainfix &lt;=c0V11FAainfix =anthV12V1anthainfix +V2V12V0Iainfix &lt;=c0V12FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter search_loop.4.1"
locfile="../vstte10_search_list.mlw"
......@@ -312,7 +304,7 @@
expl="1."
sum="3088344e503ba66b73e0f7b0c78bed63"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;=c0V4Iainfix =V6V5FICfaNilainfix =V5V7aConswVV1FINainfix =V1aNilIainfix =V4ainfix +V2c1FINainfix =V3c0ICfaNilainfix =V3V8aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV9V0aSomec0Iainfix &lt;V9V2Aainfix &lt;=c0V9FAainfix =anthV10V1anthainfix +V2V10V0Iainfix &lt;=c0V10FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -348,7 +340,7 @@
expl="2."
sum="d19e7dd6a965b922eae6b1fb94f4e942"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix +V4alengthV6alengthV0Iainfix =V6V5FICfaNilainfix =V5V7aConswVV1FINainfix =V1aNilIainfix =V4ainfix +V2c1FINainfix =V3c0ICfaNilainfix =V3V8aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV9V0aSomec0Iainfix &lt;V9V2Aainfix &lt;=c0V9FAainfix =anthV10V1anthainfix +V2V10V0Iainfix &lt;=c0V10FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -384,7 +376,7 @@
expl="3."
sum="3b7ad63c9b3b1dcc3fe922480257a257"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =anthV7V6anthainfix +V4V7V0Iainfix &lt;=c0V7FIainfix =V6V5FICfaNilainfix =V5V8aConswVV1FINainfix =V1aNilIainfix =V4ainfix +V2c1FINainfix =V3c0ICfaNilainfix =V3V9aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV10V0aSomec0Iainfix &lt;V10V2Aainfix &lt;=c0V10FAainfix =anthV11V1anthainfix +V2V11V0Iainfix &lt;=c0V11FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -405,7 +397,7 @@
expl="4."
sum="d2d905dbd8a49a94877e687830a4fb95"
proved="true"
expanded="true"
expanded="false"
shape="Nainfix =anthV7V0aSomec0Iainfix &lt;V7V4Aainfix &lt;=c0V7FIainfix =V6V5FICfaNilainfix =V5V8aConswVV1FINainfix =V1aNilIainfix =V4ainfix +V2c1FINainfix =V3c0ICfaNilainfix =V3V9aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV10V0aSomec0Iainfix &lt;V10V2Aainfix &lt;=c0V10FAainfix =anthV11V1anthainfix +V2V11V0Iainfix &lt;=c0V11FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -428,7 +420,7 @@
expl="5. loop variant decrease"
sum="50df0f2997ba8aa98b9d1840cbcf1954"
proved="true"
expanded="true"
expanded="false"
shape="loop variant decreaseCfaNilainfix =V7V6aConswVV1Iainfix =V6V5FICfaNilainfix =V5V8aConswVV1FINainfix =V1aNilIainfix =V4ainfix +V2c1FINainfix =V3c0ICfaNilainfix =V3V9aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV10V0aSomec0Iainfix &lt;V10V2Aainfix &lt;=c0V10FAainfix =anthV11V1anthainfix +V2V11V0Iainfix &lt;=c0V11FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -464,7 +456,7 @@
expl="6. postcondition"
sum="79f69c6d385733dfa65985973a2da4ed"
proved="true"
expanded="true"
expanded="false"
shape="postconditionano_zeroV0Aainfix =V2alengthV0Oazero_atV0V2Aainfix &lt;V2alengthV0Aainfix &lt;=c0V2INNainfix =V3c0ICfaNilainfix =V3V4aConsVwV1FINainfix =V1aNilINainfix =V1aNilINainfix =anthV5V0aSomec0Iainfix &lt;V5V2Aainfix &lt;=c0V5FAainfix =anthV6V1anthainfix +V2V6V0Iainfix &lt;=c0V6FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......@@ -485,7 +477,7 @@
expl="7. postcondition"
sum="155b980762af9de4f94fd68bad7d6628"
proved="true"
expanded="true"
expanded="false"
shape="postconditionano_zeroV0Aainfix =V2alengthV0Oazero_atV0V2Aainfix &lt;V2alengthV0Aainfix &lt;=c0V2INNainfix =V1aNilINainfix =anthV3V0aSomec0Iainfix &lt;V3V2Aainfix &lt;=c0V3FAainfix =anthV4V1anthainfix +V2V4V0Iainfix &lt;=c0V4FAainfix =ainfix +V2alengthV1alengthV0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for search_loop"/>
......
This diff is collapsed.
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