examples/algo65.mlw

   1 (***
   2
   3 Algorithm 65
   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 Algo65
  15
  16   use int.Int
  17   use ref.Ref
  18   use array.Array
  19   use array.ArrayPermut
  20
  21   (* algorithm 63 *)
  22
  23   val partition (a: array int) (m n: int) (i j: ref int) (ghost x: ref int) :
  24     unit
  25     requires { 0 <= m < n < length a }
  26     writes   { a, i, j }
  27     ensures  { m <= !j < !i <= n }
  28     ensures  { permut_sub (old a) a m (n+1) }
  29     ensures  { forall r:int. m <= r <= !j -> a[r] <= !x }
  30     ensures  { forall r:int. !j < r < !i -> a[r] = !x }
  31     ensures  { forall r:int. !i <= r <= n -> a[r] >= !x }
  32
  33   (* Algorithm 65 (fixed version) *)
  34
  35   let rec find (a: array int) (m n: int) (k: int) : unit
  36     requires { 0 <= m <= k <= n < length a }
  37     variant  { n - m }
  38     ensures  { permut_sub (old a) a m (n+1) }
  39     ensures  { forall r:int. m <= r <= k -> a[r] <= a[k] }
  40     ensures  { forall r:int. k <= r <= n -> a[k] <= a[r] }
  41   = if m < n then begin
  42       let i = ref 0 in
  43       let j = ref 0 in
  44       let ghost x = ref 42 in
  45       partition a m n i j x;
  46     label L1 in
  47       if k <= !j then find a m !j k;
  48       assert { permut_sub (a at L1) a m (n+1) };
  49       assert { forall r:int. !j < r <= n -> a[r] = (a at L1)[r] };
  50       assert { forall r:int. m <= r <= !j ->
  51         (exists s:int. m <= s <= !j /\ a[r] = (a at L1)[s]) &&
  52         a[r] <= a[!j+1] };
  53     label L2 in
  54       if !i <= k then find a !i n k;
  55       assert { permut_sub (a at L2) a m (n+1) };
  56       assert { forall r:int. m <= r < !i -> a[r] = (a at L2)[r] };
  57       assert { forall r:int. !i <= r <= n ->
  58         (exists s:int. !i <= s <= n /\ a[r] = (a at L2)[s]) &&
  59         a[r] >= a[!i-1] }
  60     end
  61
  62 end