algo63.mlw 2.85 KB
Newer Older
1 2 3
(***

Algorithm 63
4 5

C. A. R. Hoare
6 7 8 9
Elliott Brothers Ltd., Hertfordshire, England, U.K.

Communications of the ACM  archive
Volume 4 ,  Issue 7  (July 1961) table of contents
10
Pages: 321 - 322
11 12 13 14 15 16

***)

module Algo63

  use import int.Int
17 18 19
  use import ref.Refint
  use import array.Array
  use import array.ArrayPermut
20

21 22 23
  (* we pass m and n (as ghost arguments) to ensure [permut_sub];
     this will help solvers in the proof of partition *)
  let exchange (a: array int) (ghost m n: int) (i j: int) =
24 25 26
    requires { 0 <= m <= i <= n < length a /\ m <= j <= n }
    ensures  { exchange (old a) a i j }
    ensures  { permut_sub (old a) a m (n+1) }
27 28 29 30
    let v = a[i] in
    a[i] <- a[j];
    a[j] <- v

31
  val random (m n: int) : int ensures { m <= result <= n }
32

33
  let partition_ (a: array int) (m n: int) (i j: ref int) (ghost ghx: ref int) =
34 35 36 37 38 39
    requires { 0 <= m < n < length a }
    ensures  { m <= !j < !i <= n }
    ensures  { permut_sub (old a) a m (n+1) }
    ensures  { forall r:int. m <= r <= !j -> a[r] <= !ghx }
    ensures  { forall r:int. !j < r < !i -> a[r] = !ghx }
    ensures  { forall r:int. !i <= r <= n -> a[r] >= !ghx }
40 41 42
'Init:
    let f = random m n in
    let x = a[f] in
43
    ghx := x;
44 45 46
    i := m;
    j := n;
    let rec up_down () variant { 1 + !j - !i } =
47 48 49 50 51 52 53 54 55 56 57 58
      requires { m <= !j <= n /\ m <= !i <= n }
      requires { permut_sub (at a 'Init) a m (n+1) }
      requires { forall r:int. m <= r < !i -> a[r] <= x }
      requires { forall r:int. !j < r <= n -> a[r] >= x }
      requires { a[f] = x }
      ensures  { m <= !j <= !i <= n }
      ensures  { permut_sub (at a 'Init) a m (n+1) }
      ensures  { !i = n \/ a[!i] > x }
      ensures  { !j = m \/ a[!j] < x }
      ensures  { a[f] = x }
      ensures  { forall r:int. m <= r < !i -> a[r] <= x }
      ensures  { forall r:int. !j < r <= n -> a[r] >= x }
59
      while !i < n && a[!i] <= x do
60 61
        invariant { m <= !i <= n }
        invariant {forall r: int. m <= r < !i -> a[r] <= x }
62 63 64 65
        variant { n - !i }
        incr i
      done;
      while m < !j && a[!j] >= x do
66 67
        invariant { m <= !j <= n }
        invariant { forall r: int. !j < r <= n -> a[r] >= x }
68 69 70 71 72 73 74 75 76 77 78 79 80 81
        variant { !j }
        decr j
      done;
      if !i < !j then begin
        exchange a m n !i !j;
        incr i;
        decr j;
        up_down ()
      end
    in
    up_down ();
    assert { !j < !i \/ !j = !i = m \/ !j = !i = n };
    if !i < f then begin exchange a m n !i f; incr i end
    else if f < !j then begin exchange a m n f !j; decr j end
82 83

  let partition (a: array int) (m n: int) (i j: ref int) =
84 85 86 87
    requires { 0 <= m < n < length a }
    ensures  { m <= !j < !i <= n }
    ensures  { permut_sub (old a) a m (n+1) }
    ensures  { exists x: int.
Andrei Paskevich's avatar
Andrei Paskevich committed
88 89
        (forall r:int. m <= r <= !j -> a[r] <= x) /\
        (forall r:int. !j < r < !i -> a[r] = x) /\
90
        (forall r:int. !i <= r <= n -> a[r] >= x) }
91
    partition_ a m n i j (ref 0)
92 93

end