examples/pancake_sorting.mlw

   1
   2 (** {1 Pancake sorting}
   3
   4    See {h <a href="https://en.wikipedia.org/wiki/Pancake_sorting">Pancake
   5    sorting</a>}.
   6
   7    Author: Jean-Christophe Filliâtre (CNRS)
   8 *)
   9
  10 use mach.int.Int
  11 use ref.Ref
  12 use array.Array
  13 use array.ArraySwap
  14 use array.ArrayPermut
  15
  16 (** We choose to have the bottom of the stack of pancakes at `a[0]`.
  17     So it means we sort the array in reverse order. *)
  18
  19 predicate sorted (a: array int) (hi: int) =
  20   forall j1 j2. 0 <= j1 <= j2 < hi -> a[j1] >= a[j2]
  21
  22 (** Insert the spatula at index `i` and flip the pancakes *)
  23 let flip (a: array int) (i: int)
  24   requires { 0 <= i < length a }
  25   ensures  { forall j. 0 <= j < i        -> a[j] = (old a)[j] }
  26   ensures  { forall j. i <= j < length a -> a[j] = (old a)[length a -1-(j-i)] }
  27   ensures  { permut_all (old a) a }
  28 = let n = length a in
  29   for k = 0 to (n - i) / 2 - 1 do
  30     invariant { forall j. 0   <= j < i   -> a[j] = (old a)[j]     }
  31     invariant { forall j. i   <= j < i+k -> a[j] = (old a)[n-1-(j-i)] }
  32     invariant { forall j. i+k <= j < n-k -> a[j] = (old a)[j]     }
  33     invariant { forall j. n-k <= j < n   -> a[j] = (old a)[n-1-(j-i)] }
  34     invariant { permut_all (old a) a }
  35     swap a (i + k) (n - 1 - k)
  36   done
  37
  38 let pancake_sort (a: array int)
  39   ensures { sorted a (length a) }
  40   ensures { permut_all (old a) a }
  41 = for i = 0 to length a - 2 do
  42     invariant { sorted a i }
  43     invariant { forall j1 j2. 0 <= j1 < i <= j2 < length a -> a[j1] >= a[j2] }
  44     invariant { permut_all (old a) a }
  45     (* 1. look for the maximum of a[i..] *)
  46     let m = ref i in
  47     for k = i + 1 to length a - 1 do
  48       invariant { i <= !m < length a }
  49       invariant { forall j. i <= j < k -> a[j] <= a[!m] }
  50       if a[k] > a[!m] then m := k
  51     done;
  52     (* 2. then flip the pancakes to put it at index i *)
  53     if !m = i then continue;
  54     if !m < length a - 1 then flip a !m;
  55     flip a i
  56   done