examples/algo63.mlw

   1 (***
   2
   3 Algorithm 63
   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 Algo63
  15
  16   use int.Int
  17   use ref.Refint
  18   use array.Array
  19   use array.ArrayPermut
  20
  21   (* we pass m and n (as ghost arguments) to ensure [permut_sub];
  22      this will help solvers in the proof of partition *)
  23   let exchange (a: array int) (ghost m n: int) (i j: int) =
  24     requires { 0 <= m <= i <= n < length a /\ m <= j <= n }
  25     ensures  { exchange (old a) a i j }
  26     ensures  { permut_sub (old a) a m (n+1) }
  27     let v = a[i] in
  28     a[i] <- a[j];
  29     a[j] <- v;
  30     assert { exchange (old a) a i j }
  31
  32   val random (m n: int) : int ensures { m <= result <= n }
  33
  34   let partition_ (a: array int) (m n: int) (i j: ref int) (ghost ghx: ref int)
  35     requires { 0 <= m < n < length a }
  36     ensures  { m <= !j < !i <= n }
  37     ensures  { permut_sub (old a) a m (n+1) }
  38     ensures  { forall r:int. m <= r <= !j -> a[r] <= !ghx }
  39     ensures  { forall r:int. !j < r < !i -> a[r] = !ghx }
  40     ensures  { forall r:int. !i <= r <= n -> a[r] >= !ghx }
  41   =
  42     let f = random m n in
  43     let x = a[f] in
  44     ghx := x;
  45     i := m;
  46     j := n;
  47     let rec up_down () variant { 1 + !j - !i } =
  48       requires { m <= !j <= n /\ m <= !i <= n }
  49       requires { permut_sub (old a) a m (n+1) }
  50       requires { forall r:int. m <= r < !i -> a[r] <= x }
  51       requires { forall r:int. !j < r <= n -> a[r] >= x }
  52       requires { a[f] = x }
  53       ensures  { m <= !j <= !i <= n }
  54       ensures  { permut_sub (old a) a m (n+1) }
  55       ensures  { !i = n \/ a[!i] > x }
  56       ensures  { !j = m \/ a[!j] < x }
  57       ensures  { a[f] = x }
  58       ensures  { forall r:int. m <= r < !i -> a[r] <= x }
  59       ensures  { forall r:int. !j < r <= n -> a[r] >= x }
  60       while !i < n && a[!i] <= x do
  61         invariant { m <= !i <= n }
  62         invariant {forall r: int. m <= r < !i -> a[r] <= x }
  63         variant { n - !i }
  64         incr i
  65       done;
  66       while m < !j && a[!j] >= x do
  67         invariant { m <= !j <= n }
  68         invariant { forall r: int. !j < r <= n -> a[r] >= x }
  69         variant { !j }
  70         decr j
  71       done;
  72       if !i < !j then begin
  73         exchange a m n !i !j;
  74         incr i;
  75         decr j;
  76         up_down ()
  77       end
  78     in
  79     up_down ();
  80     assert { !j < !i \/ !j = !i = m \/ !j = !i = n };
  81     if !i < f then begin exchange a m n !i f; incr i end
  82     else if f < !j then begin exchange a m n f !j; decr j end
  83
  84   let partition (a: array int) (m n: int) (i j: ref int) =
  85     requires { 0 <= m < n < length a }
  86     ensures  { m <= !j < !i <= n }
  87     ensures  { permut_sub (old a) a m (n+1) }
  88     ensures  { exists x: int.
  89         (forall r:int. m <= r <= !j -> a[r] <= x) /\
  90         (forall r:int. !j < r < !i -> a[r] = x) /\
  91         (forall r:int. !i <= r <= n -> a[r] >= x) }
  92     partition_ a m n i j (ref 0)
  93
  94 end