Skip to content

GitLab

why3
why3
Commit 589f0297 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

more use of module array.ArraySwap in examples

parent dd3790af
Hide whitespace changes
Inline Side-by-side
Showing with 243 additions and 264 deletions
examples/quicksort.mlw
View file @ 589f0297
......@@ -11,16 +11,10 @@ module Quicksort
use import ref.Ref
use import array.Array
use import array.ArraySorted
use import array.ArraySwap
use import array.ArrayPermut
use import array.ArrayEq
let swap (t:array int) (i:int) (j:int)
requires { 0 <= i < length t /\ 0 <= j < length t }
ensures { exchange (old t) t i j }
= let v = t[i] in
t[i] <- t[j];
t[j] <- v
let rec quick_rec (t:array int) (l:int) (r:int) : unit variant { 1+r-l }
requires { 0 <= l /\ r < length t }
ensures { sorted_sub t l (r+1) /\ permut_sub (old t) t l (r+1) }
......
examples/quicksort/why3session.xml
View file @ 589f0297
......@@ -24,39 +24,19 @@
<file
name="../quicksort.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="Quicksort"
locfile="../quicksort.mlw"
loclnum="8" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="WP_parameter swap"
locfile="../quicksort.mlw"
loclnum="17" loccnumb="6" loccnume="10"
expl="VC for swap"
sum="a0e6aa0a260c53425d59522095d19ea6"
proved="true"
expanded="false"
shape="aexchangeV3V5V1V2Iainfix =V5asetV4V2agetV3V1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0V2Iainfix =V4asetV3V1agetV3V2Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
<label
name="expl:VC for swap"/>
<proof
prover="0"
timelimit="29"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
expanded="false">
<goal
name="WP_parameter quick_rec"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="VC for quick_rec"
sum="4ddc5e699aa1031a1ecbbcd81c53fc78"
sum="34f53c514e404f0a819c420edb3b6bc6"
proved="true"
expanded="false"
shape="iainfix &lt;V1V2apermut_subV3V9V1ainfix +V2c1Aasorted_subV9V1ainfix +V2c1Iapermut_subV8V9ainfix +V5c1ainfix +V2c1Aasorted_subV9ainfix +V5c1ainfix +V2c1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0ainfix +V5c1Aainfix &lt;ainfix -ainfix +c1V2ainfix +V5c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FAainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V5c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FAainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10ainfix +V2c1Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FAiainfix &lt;agetV6V12V4ainfix &lt;V13ainfix +V12c1Aainfix &lt;=V1V13Aainfix =agetV14V1V4Aapermut_subV3V14V1ainfix +V2c1Aainfix &gt;=agetV14V15V4Iainfix &lt;V15ainfix +V12c1Aainfix &lt;V13V15FAainfix &lt;agetV14V16V4Iainfix &lt;=V16V13Aainfix &lt;V1V16FIaexchangeV6V14V12V13Aainfix &lt;=c0V0FAainfix &lt;V13V0Aainfix &lt;=c0V13Aainfix &lt;V12V0Aainfix &lt;=c0V12Iainfix =V13ainfix +V5c1Fainfix &lt;V5ainfix +V12c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V17V4Iainfix &lt;V17ainfix +V12c1Aainfix &lt;V5V17FAainfix &lt;agetV6V18V4Iainfix &lt;=V18V5Aainfix &lt;V1V18FAainfix &lt;V12V0Aainfix &lt;=c0V12Aainfix &lt;=c0V0Iainfix &lt;V5V12Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V19V4Iainfix &lt;V19V12Aainfix &lt;V5V19FAainfix &lt;agetV6V20V4Iainfix &lt;=V20V5Aainfix &lt;V1V20FIainfix &lt;=V12V2Aainfix &lt;=ainfix +V1c1V12FFAainfix &lt;V1ainfix +V1c1Aainfix &lt;=V1V1Aainfix =agetV3V1V4Aapermut_subV3V3V1ainfix +V2c1Aainfix &gt;=agetV3V21V4Iainfix &lt;V21ainfix +V1c1Aainfix &lt;V1V21FAainfix &lt;agetV3V22V4Iainfix &lt;=V22V1Aainfix &lt;V1V22FIainfix &lt;=ainfix +V1c1V2Aapermut_subV3V25V1ainfix +V2c1Aasorted_subV25V1ainfix +V2c1Iapermut_subV24V25ainfix +V1c1ainfix +V2c1Aasorted_subV25ainfix +V1c1ainfix +V2c1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Aainfix &lt;ainfix -ainfix +c1V2ainfix +V1c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV23V24V1ainfix +ainfix -V1c1c1Aasorted_subV24V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FAainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V23V1V1Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Aainfix &lt;V1V0Aainfix &lt;=c0V1apermut_subV3V3V1ainfix +V2c1Aasorted_subV3V1ainfix +V2c1Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -69,9 +49,9 @@
<goal
name="WP_parameter quick_rec.1"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="1. precondition"
sum="7d7d458ce0222f4ca64b04957075c924"
sum="ae55f23d05a29688d2376eef9e4a7ddd"
proved="true"
expanded="false"
shape="ainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -89,9 +69,9 @@
<goal
name="WP_parameter quick_rec.2"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="2. precondition"
sum="dc7f7efa7c91b9e6087c61384e786bed"
sum="9bb991b2cba89d0983fceaa804cb4a3d"
proved="true"
expanded="false"
shape="ainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -109,9 +89,9 @@
<goal
name="WP_parameter quick_rec.3"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="3. variant decrease"
sum="3bb71daf7aad1d4e72e29acdd4a0a2d7"
sum="4d6cd8629305d4e566e1b967232e839a"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -129,9 +109,9 @@
<goal
name="WP_parameter quick_rec.4"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="4. precondition"
sum="227a6856b93965c5253c9a3946c401a8"
sum="9d3fd54e6e00ff8e7d4335d746a5d93b"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -149,9 +129,9 @@
<goal
name="WP_parameter quick_rec.5"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="5. variant decrease"
sum="b1e47fd51ce8162d443cd8b19edb9e69"
sum="dbadbbbfd52f6334807dfe528a3077cf"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1V2ainfix +V1c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -169,9 +149,9 @@
<goal
name="WP_parameter quick_rec.6"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="6. precondition"
sum="1b31473ddc0425cae989434e70307100"
sum="1d26d35a1ba8bc7e55f513ec21e2a46f"
proved="true"
expanded="false"
shape="ainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -189,9 +169,9 @@
<goal
name="WP_parameter quick_rec.7"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="7. postcondition"
sum="e2d09e139c07441a5c7257b1f5b07316"
sum="b9e3ed951bc33fce945efb3635bfb3c3"
proved="true"
expanded="false"
shape="apermut_subV3V7V1ainfix +V2c1Aasorted_subV7V1ainfix +V2c1Iapermut_subV6V7ainfix +V1c1ainfix +V2c1Aasorted_subV7ainfix +V1c1ainfix +V2c1Aainfix &lt;=c0V0FIainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -209,9 +189,9 @@
<goal
name="WP_parameter quick_rec.8"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="8. loop invariant init"
sum="8497b9d2e41db1c18c3a1de43e8d399e"
sum="73882fdadcde4e2c0cf821f71a5c9aa1"
proved="true"
expanded="false"
shape="ainfix &lt;V1ainfix +V1c1Aainfix &lt;=V1V1Aainfix =agetV3V1V4Aapermut_subV3V3V1ainfix +V2c1Aainfix &gt;=agetV3V5V4Iainfix &lt;V5ainfix +V1c1Aainfix &lt;V1V5FAainfix &lt;agetV3V6V4Iainfix &lt;=V6V1Aainfix &lt;V1V6FIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -229,9 +209,9 @@
<goal
name="WP_parameter quick_rec.9"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="9. type invariant"
sum="923d48918d92090b10b016a9c93ce591"
sum="1d09049de88433625160180763d59f29"
proved="true"
expanded="false"
shape="ainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8V7Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -249,9 +229,9 @@
<goal
name="WP_parameter quick_rec.10"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="10. precondition"
sum="f3383493ceefcd497194f12d4ea1eadc"
sum="de2809145aaedc84dc3b7fef0347c3f2"
proved="true"
expanded="false"
shape="ainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8V7Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -269,9 +249,9 @@
<goal
name="WP_parameter quick_rec.11"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="11. precondition"
sum="73f2b27977492b17e040e2b68904a39e"
sum="b58126fc9aaa0d3d70e0c6159fce3eae"
proved="true"
expanded="false"
shape="ainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V9V4Iainfix &lt;V9V7Aainfix &lt;V5V9FAainfix &lt;agetV6V10V4Iainfix &lt;=V10V5Aainfix &lt;V1V10FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -289,9 +269,9 @@
<goal
name="WP_parameter quick_rec.12"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="12. loop invariant preservation"
sum="6b35c535b227eded0e988b507d79590f"
sum="95889a61eecb6c9cb769f913c8ffee67"
proved="true"
expanded="false"
shape="ainfix &lt;V8ainfix +V7c1Aainfix &lt;=V1V8Aainfix =agetV9V1V4Aapermut_subV3V9V1ainfix +V2c1Aainfix &gt;=agetV9V10V4Iainfix &lt;V10ainfix +V7c1Aainfix &lt;V8V10FAainfix &lt;agetV9V11V4Iainfix &lt;=V11V8Aainfix &lt;V1V11FIaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V12V4Iainfix &lt;V12V7Aainfix &lt;V5V12FAainfix &lt;agetV6V13V4Iainfix &lt;=V13V5Aainfix &lt;V1V13FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -304,9 +284,9 @@
<goal
name="WP_parameter quick_rec.12.1"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="1."
sum="befd4786b53ca3e49b83c96878fd826c"
sum="1d45e9be4f3306bc1a448e91a350c5e4"
proved="true"
expanded="false"
shape="ainfix &lt;agetV9V10V4Iainfix &lt;=V10V8Aainfix &lt;V1V10FIaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V11V4Iainfix &lt;V11V7Aainfix &lt;V5V11FAainfix &lt;agetV6V12V4Iainfix &lt;=V12V5Aainfix &lt;V1V12FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -324,9 +304,9 @@
<goal
name="WP_parameter quick_rec.12.2"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="2."
sum="7db9a46260f71e4d3ae6ee618bfb91ba"
sum="d63df8c1733cf7fdd665dc752264e88d"
proved="true"
expanded="false"
shape="ainfix &gt;=agetV9V10V4Iainfix &lt;V10ainfix +V7c1Aainfix &lt;V8V10FIaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V11V4Iainfix &lt;V11V7Aainfix &lt;V5V11FAainfix &lt;agetV6V12V4Iainfix &lt;=V12V5Aainfix &lt;V1V12FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -344,9 +324,9 @@
<goal
name="WP_parameter quick_rec.12.3"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="3."
sum="1aaf168e515a0d857ce78f26563485b7"
sum="595f447c4093a4fab71d6f9c0e23c7e0"
proved="true"
expanded="false"
shape="apermut_subV3V9V1ainfix +V2c1IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -359,15 +339,15 @@
edited="quicksort_WP_Quicksort_WP_parameter_quick_rec_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.57"/>
<result status="valid" time="1.93"/>
</proof>
</goal>
<goal
name="WP_parameter quick_rec.12.4"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="4."
sum="8222a141c6f2a6e34f6e5c6537506687"
sum="c79f4b989159b6ce2c8c377ddd1aae0a"
proved="true"
expanded="false"
shape="ainfix =agetV9V1V4IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -385,9 +365,9 @@
<goal
name="WP_parameter quick_rec.12.5"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="5."
sum="32e820638e5c84864f26323b16cd9a59"
sum="8c671be21dd714f551823c2a8325c566"
proved="true"
expanded="false"
shape="ainfix &lt;=V1V8IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -405,9 +385,9 @@
<goal
name="WP_parameter quick_rec.12.6"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="6."
sum="be9b5da54df54578675dc2b34bc3d3fd"
sum="bc2e10a4a5d5cba20d3544d9bfc4403f"
proved="true"
expanded="false"
shape="ainfix &lt;V8ainfix +V7c1IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -427,9 +407,9 @@
<goal
name="WP_parameter quick_rec.13"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="13. loop invariant preservation"
sum="fa6637c8f4b8d011a06d0dbe0c60933e"
sum="b902f8b5c2369745284d3e4cc6acfc50"
proved="true"
expanded="false"
shape="ainfix &lt;V5ainfix +V7c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8ainfix +V7c1Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FIainfix &lt;agetV6V7V4NIainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -447,9 +427,9 @@
<goal
name="WP_parameter quick_rec.14"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="14. type invariant"
sum="5d875a08da7310ecaa75bdd83734e17a"
sum="db6ae382fccf4d1dafe7783f06496638"
proved="true"
expanded="false"
shape="ainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -467,9 +447,9 @@
<goal
name="WP_parameter quick_rec.15"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="15. precondition"
sum="63a366347d0e2ac0735db16d000c4e10"
sum="ddb72d17faf5a91da1edad9489f0d34f"
proved="true"
expanded="false"
shape="ainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -482,9 +462,9 @@
<goal
name="WP_parameter quick_rec.15.1"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="1."
sum="bef114c4ff3b3300dd85ce346fb49498"
sum="f28a60ac715732d093431611b5653bca"
proved="true"
expanded="false"
shape="ainfix &lt;=c0V1Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -502,9 +482,9 @@
<goal
name="WP_parameter quick_rec.15.2"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="2."
sum="2cf9c9b34f4ec9a84034c02bffc1d5c6"
sum="b7c0bed51260822bebe8aa68f0dc40cf"
proved="true"
expanded="false"
shape="ainfix &lt;V1V0Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -522,9 +502,9 @@
<goal
name="WP_parameter quick_rec.15.3"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="3."
sum="bffbcc5961922ed4dfca616fbf48f397"
sum="05cc1f6ece42cdd219a0ba82cc27cd81"
proved="true"
expanded="false"
shape="ainfix &lt;=c0V5Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -542,9 +522,9 @@
<goal
name="WP_parameter quick_rec.15.4"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="4."
sum="3f4e824534358868f8c7f600af3c4652"
sum="115df8ce22b7d8a5f7ac3f91dad7d931"
proved="true"
expanded="false"
shape="ainfix &lt;V5V0Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -564,9 +544,9 @@
<goal
name="WP_parameter quick_rec.16"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="16. variant decrease"
sum="e0792cb57e1cc385befecfdc6f50c9e7"
sum="737ffc650218694bcc57a9d1ae9ddd35"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1ainfix -V5c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8ainfix +V2c1Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -584,9 +564,9 @@
<goal
name="WP_parameter quick_rec.17"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="17. precondition"
sum="3cc6b6642ce915be9b41186729e66da3"
sum="9303d0dcf8380a2624871249c87e63fc"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8ainfix +V2c1Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -604,9 +584,9 @@
<goal
name="WP_parameter quick_rec.18"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="18. variant decrease"
sum="1ab79307c5c52f070c1cb3f6a74bdbe8"
sum="83e621fe3643e6c4f2ff6746404f618f"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1V2ainfix +V5c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V9V4Iainfix &lt;V9ainfix +V2c1Aainfix &lt;V5V9FAainfix &lt;agetV6V10V4Iainfix &lt;=V10V5Aainfix &lt;V1V10FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -624,9 +604,9 @@
<goal
name="WP_parameter quick_rec.19"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="19. precondition"
sum="3348dada82d7da56fbafe89a2f77ebff"
sum="548e6b4c6de6a3d686e2ba43d2197426"
proved="true"
expanded="false"
shape="ainfix &lt;V2V0Aainfix &lt;=c0ainfix +V5c1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V9V4Iainfix &lt;V9ainfix +V2c1Aainfix &lt;V5V9FAainfix &lt;agetV6V10V4Iainfix &lt;=V10V5Aainfix &lt;V1V10FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -644,9 +624,9 @@
<goal
name="WP_parameter quick_rec.20"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="20. postcondition"
sum="616cb0b075b543129a65e3b6a40d9f35"
sum="25298083d253829fe468ee94d253c22e"
proved="true"
expanded="false"
shape="apermut_subV3V9V1ainfix +V2c1Aasorted_subV9V1ainfix +V2c1Iapermut_subV8V9ainfix +V5c1ainfix +V2c1Aasorted_subV9ainfix +V5c1ainfix +V2c1Aainfix &lt;=c0V0FIainfix &lt;V2V0Aainfix &lt;=c0ainfix +V5c1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10ainfix +V2c1Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -659,15 +639,15 @@
edited="quicksort_WP_Quicksort_WP_parameter_quick_rec_2.v"
obsolete="false"
archived="false">
<result status="valid" time="1.54"/>
<result status="valid" time="5.26"/>
</proof>
</goal>
<goal
name="WP_parameter quick_rec.21"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="21. postcondition"
sum="c5a1e7c20769ef45f89992930442d82e"
sum="3ed4b87a24f191766178e9165c896a74"
proved="true"
expanded="false"
shape="apermut_subV3V3V1ainfix +V2c1Aasorted_subV3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -680,9 +660,9 @@
<goal
name="WP_parameter quick_rec.21.1"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="1."
sum="0b53241d282f56c733b2a6ac339a2f47"
sum="a33e2c171c6bbb2e3bc6574e614d8970"
proved="true"
expanded="false"
shape="asorted_subV3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -700,9 +680,9 @@
<goal
name="WP_parameter quick_rec.21.2"
locfile="../quicksort.mlw"
loclnum="24" loccnumb="10" loccnume="19"
loclnum="18" loccnumb="10" loccnume="19"
expl="2."
sum="0b87a20ff03a37864fa9be1beffff1e1"
sum="a2f76e3daa62b13a53a9375c22557c1e"
proved="true"
expanded="false"
shape="apermut_subV3V3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
......@@ -724,9 +704,9 @@
<goal
name="WP_parameter quicksort"
locfile="../quicksort.mlw"
loclnum="42" loccnumb="6" loccnume="15"
loclnum="36" loccnumb="6" loccnume="15"
expl="VC for quicksort"
sum="2f88e6d7cc71b4b729ddbf2a7da15cce"
sum="2b3422cbaca575d9ab3d2440337ffa9a"
proved="true"
expanded="false"
shape="apermutamk arrayV0V1amk arrayV0V2Aasorted_subV2c0V0Iapermut_subV1V2c0ainfix +ainfix -V0c1c1Aasorted_subV2c0ainfix +ainfix -V0c1c1Aainfix &lt;=c0V0FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0FF">
......@@ -739,9 +719,9 @@
<goal
name="WP_parameter quicksort.1"
locfile="../quicksort.mlw"
loclnum="42" loccnumb="6" loccnume="15"
loclnum="36" loccnumb="6" loccnume="15"
expl="1. precondition"
sum="7b8d37bb459cde5602e168c003588571"
sum="5393c9438f88776ff208e12eff1ebbd2"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0FF">
......@@ -775,9 +755,9 @@
<goal
name="WP_parameter quicksort.2"
locfile="../quicksort.mlw"
loclnum="42" loccnumb="6" loccnume="15"
loclnum="36" loccnumb="6" loccnume="15"
expl="2. postcondition"
sum="6a9ec9fa966fedeb71742ad86d71fa3b"
sum="4a0ecc70082b1037004b6481a0899df7"
proved="true"
expanded="false"
shape="apermutamk arrayV0V1amk arrayV0V2Aasorted_subV2c0V0Iapermut_subV1V2c0ainfix +ainfix -V0c1c1Aasorted_subV2c0ainfix +ainfix -V0c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0FF">
......
examples/selection_sort.mlw
View file @ 589f0297
......@@ -7,16 +7,10 @@ module SelectionSort
use import ref.Ref
use import array.Array
use import array.ArraySorted
use import array.ArraySwap
use import array.ArrayPermut
use import array.ArrayEq
let swap (a: array int) (i: int) (j: int)
requires { 0 <= i < length a /\ 0 <= j < length a }
ensures { exchange (old a) a i j }
= let v = a[i] in
a[i] <- a[j];
a[j] <- v
let selection_sort (a: array int)
ensures { sorted a /\ permut (old a) a } =
'L:
......
examples/selection_sort/why3session.xml
View file @ 589f0297
......@@ -19,32 +19,12 @@
loclnum="4" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
<goal
name="WP_parameter swap"
locfile="../selection_sort.mlw"
loclnum="13" loccnumb="6" loccnume="10"
expl="VC for swap"
sum="a0e6aa0a260c53425d59522095d19ea6"
proved="true"
expanded="true"
shape="aexchangeV3V5V1V2Iainfix =V5asetV4V2agetV3V1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0V2Iainfix =V4asetV3V1agetV3V2Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
<label
name="expl:VC for swap"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter selection_sort"
locfile="../selection_sort.mlw"
loclnum="20" loccnumb="6" loccnume="20"
loclnum="14" loccnumb="6" loccnume="20"
expl="VC for selection_sort"
sum="e4c8e8b6008074245574dd34437b1be4"
sum="fb250d5b3364bc18e3201530a9b1f43e"
proved="true"
expanded="true"
shape="apermutV2V4Aasorted_subV3c0V0Aainfix &lt;=c0V0Iainfix &lt;=agetV3V5agetV3V6Iainfix &lt;V6V0Aainfix &lt;=ainfix +ainfix -V0c1c1V6Aainfix &lt;V5ainfix +ainfix -V0c1c1Aainfix &lt;=c0V5FAapermutV2V4Aasorted_subV3c0ainfix +ainfix -V0c1c1Aiainfix =V8V7Nainfix &lt;=agetV9V11agetV9V12Iainfix &lt;V12V0Aainfix &lt;=ainfix +V7c1V12Aainfix &lt;V11ainfix +V7c1Aainfix &lt;=c0V11FAapermutV2V10Aasorted_subV9c0ainfix +V7c1AapermutV4V10IaexchangeV3V9V8V7Aainfix &lt;=c0V0Lamk arrayV0V9FAainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;V8V0Aainfix &lt;=c0V8ainfix &lt;=agetV3V13agetV3V14Iainfix &lt;V14V0Aainfix &lt;=ainfix +V7c1V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FAapermutV2V4Aasorted_subV3c0ainfix +V7c1AapermutV4V4Iainfix &lt;=agetV3V8agetV3V15Iainfix &lt;V15ainfix +ainfix -V0c1c1Aainfix &lt;=V7V15FAainfix &lt;V8ainfix +ainfix -V0c1c1Aainfix &lt;=V7V8Aiainfix &lt;agetV3V16agetV3V8ainfix &lt;=agetV3V17agetV3V18Iainfix &lt;V18ainfix +V16c1Aainfix &lt;=V7V18FAainfix &lt;V17ainfix +V16c1Aainfix &lt;=V7V17Iainfix =V17V16Fainfix &lt;=agetV3V8agetV3V19Iainfix &lt;V19ainfix +V16c1Aainfix &lt;=V7V19FAainfix &lt;V8ainfix +V16c1Aainfix &lt;=V7V8Aainfix &lt;V16V0Aainfix &lt;=c0V16Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix &lt;=agetV3V8agetV3V20Iainfix &lt;V20V16Aainfix &lt;=V7V20FAainfix &lt;V8V16Aainfix &lt;=V7V8Iainfix &lt;=V16ainfix -V0c1Aainfix &lt;=ainfix +V7c1V16FFAainfix &lt;=agetV3V7agetV3V21Iainfix &lt;V21ainfix +V7c1Aainfix &lt;=V7V21FAainfix &lt;V7ainfix +V7c1Aainfix &lt;=V7V7Iainfix &lt;=ainfix +V7c1ainfix -V0c1Aiainfix =V7V7Nainfix &lt;=agetV22V24agetV22V25Iainfix &lt;V25V0Aainfix &lt;=ainfix +V7c1V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FAapermutV2V23Aasorted_subV22c0ainfix +V7c1AapermutV4V23IaexchangeV3V22V7V7Aainfix &lt;=c0V0Lamk arrayV0V22FAainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;=agetV3V26agetV3V27Iainfix &lt;V27V0Aainfix &lt;=ainfix +V7c1V27Aainfix &lt;V26ainfix +V7c1Aainfix &lt;=c0V26FAapermutV2V4Aasorted_subV3c0ainfix +V7c1AapermutV4V4Iainfix &gt;ainfix +V7c1ainfix -V0c1Aainfix &lt;=c0V0Iainfix &lt;=agetV3V28agetV3V29Iainfix &lt;V29V0Aainfix &lt;=V7V29Aainfix &lt;V28V7Aainfix &lt;=c0V28FAapermutV2V4Aasorted_subV3c0V7Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=c0V7FLamk arrayV0V3FAainfix &lt;=agetV1V30agetV1V31Iainfix &lt;V31V0Aainfix &lt;=c0V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FAapermutV2V2Aasorted_subV1c0c0Iainfix &lt;=c0ainfix -V0c1AapermutV2V2Aasorted_subV1c0V0Iainfix &gt;c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
......@@ -57,11 +37,11 @@
<goal
name="WP_parameter selection_sort.1"
locfile="../selection_sort.mlw"
loclnum="20" loccnumb="6" loccnume="20"
loclnum="14" loccnumb="6" loccnume="20"
expl="1. postcondition"
sum="ca4addc2f0684b810463d843491d8209"
sum="d5603b2e01b07c07d1da8df2f4e341d7"
proved="true"
expanded="true"
expanded="false"
shape="apermutV2V2Aasorted_subV1c0V0Iainfix &gt;c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for selection_sort"/>
......@@ -77,11 +57,11 @@
<goal
name="WP_parameter selection_sort.2"
locfile="../selection_sort.mlw"
loclnum="20" loccnumb="6" loccnume="20"
loclnum="14" loccnumb="6" loccnume="20"
expl="2. loop invariant init"
sum="4a0cceb43b1dbdf006dd01fa6fc5ff97"
sum="162e12ec71e8921dc98fbe70f38ea50e"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;=agetV1V3agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V3c0Aainfix &lt;=c0V3FAapermutV2V2Aasorted_subV1c0c0Iainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for selection_sort"/>
......@@ -97,9 +77,9 @@
<goal
name="WP_parameter selection_sort.3"
locfile="../selection_sort.mlw"
loclnum="20" loccnumb="6" loccnume="20"
loclnum="14" loccnumb="6" loccnume="20"
expl="3. type invariant"
sum="06ab73e335b59abf46228bcd4a6fda75"
sum="10062dd2f2a6421903735a818555dcc6"
proved="true"
expanded="false"
shape="ainfix &lt;=c0V0Iainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7V0Aainfix &lt;=V5V7Aainfix &lt;V6V5Aainfix &lt;=c0V6FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
......@@ -117,11 +97,11 @@
<goal
name="WP_parameter selection_sort.4"
locfile="../selection_sort.mlw"
loclnum="20" loccnumb="6" loccnume="20"
loclnum="14" loccnumb="6" loccnume="20"
expl="4. precondition"
sum="6da27c14e9f9b9828ca3a46da9cc0a38"
sum="fac34059cb8168ba10feab73e1b1430c"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =V5V5NIainfix &gt;ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7V0Aainfix &lt;=V5V7Aainfix &lt;V6V5Aainfix &lt;=c0V6FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for selection_sort"/>
......@@ -137,11 +117,11 @@
<goal
name="WP_parameter selection_sort.5"
locfile="../selection_sort.mlw"
loclnum="20" loccnumb="6" loccnume="20"
loclnum="14" loccnumb="6" loccnume="20"
expl="5. assertion"
sum="59bd7bcd22319d568925a9b2b69f15c6"
sum="bfae1bce6420af6349c332fc4c1c4b8a"
proved="true"
expanded="true"
expanded="false"
shape="apermutV4V7IaexchangeV3V6V5V5Aainfix &lt;=c0V0Lamk arrayV0V6FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =V5V5NIainfix &gt;ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V8agetV3V9Iainfix &lt;V9V0Aainfix &lt;=V5V9Aainfix &lt;V8V5Aainfix &lt;=c0V8FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for selection_sort"/>
......@@ -157,11 +137,11 @@
<goal
name="WP_parameter selection_sort.6"
locfile="../selection_sort.mlw"
loclnum="20" loccnumb="6" loccnume="20"
loclnum="14" loccnumb="6" loccnume="20"
expl="6. loop invariant preservation"
sum="323b675790a18c07d41f29cc6c525284"
sum="6316be2d386c486479b029643e05810b"