examples/algo64.mlw

   1 (***
   2
   3 Algorithm 64
   4
   5 C. A. R. Hoare
   6 Elliott Brothers Ltd., Hertfordshire, England, U.K.
   7
   8 Communications of the ACM  archive
   9 Volume 4 ,  Issue 7  (July 1961) table of contents
  10 Pages: 321 - 322
  11
  12 ***)
  13
  14 module Algo64
  15
  16   use int.Int
  17   use ref.Ref
  18   use array.Array
  19   use array.ArrayPermut
  20   use array.IntArraySorted
  21
  22   (* Algorithm 63 *)
  23
  24   val partition (a: array int) (m n: int) (i j: ref int) (ghost x: ref int) :
  25     unit
  26     requires { 0 <= m < n < length a }
  27     writes   { a, i, j }
  28     ensures  { m <= !j < !i <= n }
  29     ensures  { permut_sub (old a) a m (n+1) }
  30     ensures  { forall r:int. m <= r <= !j -> a[r] <= !x }
  31     ensures  { forall r:int. !j < r < !i -> a[r] = !x }
  32     ensures  { forall r:int. !i <= r <= n -> a[r] >= !x }
  33
  34   (* Algorithm 64 *)
  35
  36   predicate qs_partition (t1 t2: array int) (m n i j: int) (x: int) =
  37     permut_sub t1 t2 m (n+1) /\
  38     (forall k:int. m <= k <= j  -> t2[k] <= x) /\
  39     (forall k:int. j <  k <  i  -> t2[k] =  x) /\
  40     (forall k:int. i <= k <= n ->  t2[k] >= x)
  41
  42   let rec quicksort (a:array int) (m n:int) : unit
  43     requires { 0 <= m <= n < length a }
  44     variant  { n - m }
  45     ensures  { permut_sub (old a) a m (n+1) }
  46     ensures  { sorted_sub a m (n+1) }
  47   = if m < n then begin
  48       let i = ref 0 in
  49       let j = ref 0 in
  50       let ghost x = ref 42 in
  51       partition a m n i j x;
  52     label L1 in
  53       quicksort a m !j;
  54       assert { qs_partition (a at L1) a m n !i !j !x };
  55     label L2 in
  56       quicksort a !i n;
  57       assert { qs_partition (a at L2) a m n !i !j !x }
  58     end
  59
  60   let qs (a:array int) : unit
  61     ensures  { permut_all (old a) a }
  62     ensures  { sorted a }
  63   = if length a > 0 then quicksort a 0 (length a - 1)
  64
  65 end