updated sessions

parent 37cafd50
......@@ -56,7 +56,7 @@ module Algo64
end
let qs (a:array int) : unit
ensures { permut_all (old a) a /\ qs_partition (old a) a 0 0 0 0 0 }
ensures { permut_all (old a) a }
ensures { sorted a }
= if length a > 0 then quicksort a 0 (length a - 1)
......
......@@ -20,7 +20,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="VC for quicksort"
sum="e5a95e1ad0ea256fea9c1f9fad319b7e"
sum="f043ca9eecd283c33d3aa095f417529e"
proved="true"
expanded="true"
shape="iasorted_subV1V2ainfix +V3c1Aapermut_subV4V4V2ainfix +V3c1asorted_subV11V2ainfix +V3c1Aapermut_subV4V12V2ainfix +V3c1Aaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FAainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Aainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Aaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FAainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Aainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FAainfix <V3V0Aainfix <V2V3Aainfix <=c0V2ainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -35,7 +35,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="1. precondition"
sum="8379b04eca91ec72dcc0de90d79a33c9"
sum="baec3fa427ab9f37e9870b6b2a87406b"
proved="true"
expanded="false"
shape="preconditionainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -55,7 +55,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="2. variant decrease"
sum="1c49a9d502846caa13ec8b9a73c6b360"
sum="61b814478a17acf70c264f5b499fcf68"
proved="true"
expanded="false"
shape="variant decreaseainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -75,7 +75,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="3. precondition"
sum="aa4da5326f81bb86b444d156ea839ce3"
sum="e1bf5835eed6c1a7ce4b27ed2653b028"
proved="true"
expanded="false"
shape="preconditionainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -95,7 +95,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="4. assertion"
sum="87d83ab329ca664125ad74803e68eb36"
sum="d3e70c476739ee31ff1e2a95036a92aa"
proved="true"
expanded="false"
shape="assertionaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -115,7 +115,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="5. variant decrease"
sum="f9cbf74723eb86d38415b9f5596ad488"
sum="5903ec9535586c4861b3d99dcb5d8704"
proved="true"
expanded="false"
shape="variant decreaseainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -135,7 +135,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="6. precondition"
sum="5b85faecc758127a0a82396dabda258b"
sum="b0224b26d7c793c8b9c6e798c4554e08"
proved="true"
expanded="false"
shape="preconditionainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -155,7 +155,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="7. assertion"
sum="4756864241cad7200c6b1876b7451340"
sum="ef1b2c49464f03bc88f8b524e37fe0e7"
proved="true"
expanded="false"
shape="assertionaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -167,7 +167,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.80"/>
<result status="valid" time="2.01"/>
</proof>
</goal>
<goal
......@@ -175,7 +175,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="8. postcondition"
sum="9c76253f9d4d2b60a254999b89e81e75"
sum="5315ed698b5d8ed526953991c4358f71"
proved="true"
expanded="false"
shape="postconditionapermut_subV4V12V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V11FIainfix &lt;V3V0Aainfix &lt;=V6V3Aainfix &lt;=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix &lt;=c0V0Lamk arrayV0V9FIainfix &lt;V5V0Aainfix &lt;=V2V5Aainfix &lt;=c0V2Iainfix &gt;=agetV7V13c42Iainfix &lt;=V13V3Aainfix &lt;=V6V13FAainfix =agetV7V14c42Iainfix &lt;V14V6Aainfix &lt;V5V14FAainfix &lt;=agetV7V15c42Iainfix &lt;=V15V5Aainfix &lt;=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix &lt;=V6V3Aainfix &lt;V5V6Aainfix &lt;=V2V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -195,7 +195,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="9. postcondition"
sum="da78dcb78a5a66e1231bc515474b093a"
sum="6ebdeca09c4e0b5cb6f7f4ed95839824"
proved="true"
expanded="false"
shape="postconditionasorted_subV11V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V11FIainfix &lt;V3V0Aainfix &lt;=V6V3Aainfix &lt;=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix &lt;=c0V0Lamk arrayV0V9FIainfix &lt;V5V0Aainfix &lt;=V2V5Aainfix &lt;=c0V2Iainfix &gt;=agetV7V13c42Iainfix &lt;=V13V3Aainfix &lt;=V6V13FAainfix =agetV7V14c42Iainfix &lt;V14V6Aainfix &lt;V5V14FAainfix &lt;=agetV7V15c42Iainfix &lt;=V15V5Aainfix &lt;=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix &lt;=V6V3Aainfix &lt;V5V6Aainfix &lt;=V2V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -215,7 +215,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="10. postcondition"
sum="0b9cf33f48efcee7c5e95d15dd73ca64"
sum="f4aaa70b41b128d8f6dd9fed2fa2efcb"
proved="true"
expanded="false"
shape="postconditionapermut_subV4V4V2ainfix +V3c1INainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -235,7 +235,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="11. postcondition"
sum="e0b81adf57da9dabe54f9a309f22f12e"
sum="f961cba67d14248c04b5027e2abec1e5"
proved="true"
expanded="false"
shape="postconditionasorted_subV1V2ainfix +V3c1INainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -255,9 +255,9 @@
<goal
name="WP_parameter qs"
locfile="../algo64.mlw"
loclnum="80" loccnumb="6" loccnume="8"
loclnum="58" loccnumb="6" loccnume="8"
expl="VC for qs"
sum="a036cd8d73e3142e9d97955f722756bf"
sum="620e6ca3e385dbb67091edda8b3f4874"
proved="true"
expanded="false"
shape="iasorted_subV1c0V0Aapermut_allV2V2asorted_subV4c0V0Aapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V4FAainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1ainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -270,9 +270,9 @@
<goal
name="WP_parameter qs.1"
locfile="../algo64.mlw"
loclnum="80" loccnumb="6" loccnume="8"
loclnum="58" loccnumb="6" loccnume="8"
expl="1. precondition"
sum="0e7d90b24d523e2e364bcbb6a7fbb96b"
sum="cfeef4869dd91a4c4eaa642d6b6837c8"
proved="true"
expanded="false"
shape="preconditionainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1Iainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -290,9 +290,9 @@
<goal
name="WP_parameter qs.2"
locfile="../algo64.mlw"
loclnum="80" loccnumb="6" loccnume="8"
loclnum="58" loccnumb="6" loccnume="8"
expl="2. postcondition"
sum="b1faf202ab7f4a38a1ad63dabeff1057"
sum="dd935033668b4af88b757f7e24d45909"
proved="true"
expanded="false"
shape="postconditionapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V4FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1Iainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -310,9 +310,9 @@
<goal
name="WP_parameter qs.3"
locfile="../algo64.mlw"
loclnum="80" loccnumb="6" loccnume="8"
loclnum="58" loccnumb="6" loccnume="8"
expl="3. postcondition"
sum="f706c2ec3b18518722154bdeb342227b"
sum="50540c91c27a7611995c0c91ae4874e7"
proved="true"
expanded="false"
shape="postconditionasorted_subV4c0V0Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V4FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1Iainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -330,9 +330,9 @@
<goal
name="WP_parameter qs.4"
locfile="../algo64.mlw"
loclnum="80" loccnumb="6" loccnume="8"
loclnum="58" loccnumb="6" loccnume="8"
expl="4. postcondition"
sum="1031231ffb9f2858c92529495763574a"
sum="6f46afd8f3a5e8f82e38d25f39b37c0a"
proved="true"
expanded="false"
shape="postconditionapermut_allV2V2INainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -350,9 +350,9 @@
<goal
name="WP_parameter qs.5"
locfile="../algo64.mlw"
loclnum="80" loccnumb="6" loccnume="8"
loclnum="58" loccnumb="6" loccnume="8"
expl="5. postcondition"
sum="01d281b3e4e6563e63e5f44b215d4bce"
sum="cf95c3c36f0ec712ce8df01b60098dec"
proved="true"
expanded="false"
shape="postconditionasorted_subV1c0V0INainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......
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