new example: pancake sorting

parent cdb47d44
(** {1 Pancake sorting}
See {h <a href="https://en.wikipedia.org/wiki/Pancake_sorting">Pancake
sorting</a>}.
Author: Jean-Christophe Filliâtre (CNRS)
*)
use mach.int.Int
use ref.Ref
use array.Array
use array.ArraySwap
use array.ArrayPermut
(** We choose to have the bottom of the stack of pancakes at `a[0]`.
So it means we sort the array in reverse order. *)
predicate sorted (a: array int) (hi: int) =
forall j1 j2. 0 <= j1 <= j2 < hi -> a[j1] >= a[j2]
(** Insert the spatula at index `i` and flip the pancakes *)
let flip (a: array int) (i: int)
requires { 0 <= i < length a }
ensures { forall j. 0 <= j < i -> a[j] = (old a)[j] }
ensures { forall j. i <= j < length a -> a[j] = (old a)[length a -1-(j-i)] }
ensures { permut_all (old a) a }
= let n = length a in
for k = 0 to (n - i) / 2 - 1 do
invariant { forall j. 0 <= j < i -> a[j] = (old a)[j] }
invariant { forall j. i <= j < i+k -> a[j] = (old a)[n-1-(j-i)] }
invariant { forall j. i+k <= j < n-k -> a[j] = (old a)[j] }
invariant { forall j. n-k <= j < n -> a[j] = (old a)[n-1-(j-i)] }
invariant { permut_all (old a) a }
swap a (i + k) (n - 1 - k)
done
let pancake_sort (a: array int)
ensures { sorted a (length a) }
ensures { permut_all (old a) a }
= for i = 0 to length a - 2 do
invariant { sorted a i }
invariant { forall j1 j2. 0 <= j1 < i <= j2 < length a -> a[j1] >= a[j2] }
invariant { permut_all (old a) a }
(* 1. look for the maximum of a[i..] *)
let m = ref i in
for k = i + 1 to length a - 1 do
invariant { i <= !m < length a }
invariant { forall j. i <= j < k -> a[j] <= a[!m] }
if a[k] > a[!m] then m := k
done;
(* 2. then flip the pancakes to put it at index i *)
if !m = i then continue;
if !m < length a - 1 then flip a !m;
flip a i
done
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../pancake_sorting.mlw" proved="true">
<theory name="Top" proved="true">
<goal name="VC flip" expl="VC for flip" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC flip.0" expl="check division by zero" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC flip.1" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC flip.2" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC flip.3" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC flip.4" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC flip.5" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC flip.6" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC flip.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC flip.8" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC flip.9" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC flip.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC flip.11" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC flip.12" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC flip.13" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC flip.14" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC flip.15" expl="out of loop bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC pancake_sort" expl="VC for pancake_sort" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC pancake_sort.0" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.1" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.2" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.3" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.4" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.5" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.6" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.8" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.9" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC pancake_sort.12" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.13" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.14" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.15" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.16" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC pancake_sort.17" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC pancake_sort.18" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.19" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC pancake_sort.20" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC pancake_sort.21" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC pancake_sort.22" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.23" expl="out of loop bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.24" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC pancake_sort.25" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pancake_sort.26" expl="out of loop bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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