Pancake sorting
Sort a pile of pancakes by only flipping the top ones
Authors: Jean-Christophe Filliâtre
Topics: Sorting Algorithms
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
Pancake sorting
See Pancake sorting.
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] 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
Insert the spatula at index i
and flip the pancakes
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
download ZIP archive
Why3 Proof Results for Project "pancake_sorting"
Theory "pancake_sorting.Top": fully verified
Obligations | CVC4 1.5 | |
VC for flip | --- | |
split_vc | ||
check division by zero | 0.02 | |
loop invariant init | 0.02 | |
loop invariant init | 0.02 | |
loop invariant init | 0.02 | |
loop invariant init | 0.02 | |
loop invariant init | 0.04 | |
precondition | 0.03 | |
loop invariant preservation | 0.05 | |
loop invariant preservation | 0.07 | |
loop invariant preservation | 0.05 | |
loop invariant preservation | 0.06 | |
loop invariant preservation | 0.04 | |
postcondition | 0.03 | |
postcondition | 0.07 | |
postcondition | 0.02 | |
out of loop bounds | 0.03 | |
VC for pancake_sort | --- | |
split_vc | ||
loop invariant init | 0.03 | |
loop invariant init | 0.02 | |
loop invariant init | 0.03 | |
loop invariant init | 0.03 | |
loop invariant init | 0.02 | |
index in array bounds | 0.03 | |
index in array bounds | 0.03 | |
loop invariant preservation | 0.03 | |
loop invariant preservation | 0.03 | |
loop invariant preservation | 0.02 | |
loop invariant preservation | 0.03 | |
loop invariant preservation | 0.04 | |
loop invariant preservation | 0.03 | |
loop invariant preservation | 0.03 | |
precondition | 0.02 | |
precondition | 0.02 | |
loop invariant preservation | 0.09 | |
loop invariant preservation | 0.54 | |
loop invariant preservation | 0.02 | |
precondition | 0.01 | |
loop invariant preservation | 0.04 | |
loop invariant preservation | 0.05 | |
loop invariant preservation | 0.02 | |
out of loop bounds | 0.02 | |
postcondition | 0.03 | |
postcondition | 0.02 | |
out of loop bounds | 0.02 |