algo63.mlw 2.68 KB
Newer Older
1 2 3 4

(***

Algorithm 63
5 6

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

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

***)

module Algo63

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

22 23 24 25 26 27 28 29 30 31 32
  (* 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) =
    { 0 <= m <= i <= n < length a /\ m <= j <= n }
    let v = a[i] in
    a[i] <- a[j];
    a[j] <- v
    { exchange (old a) a i j /\ permut_sub (old a) a m (n+1) }

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

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

  let partition (a: array int) (m n: int) (i j: ref int) =
    { 0 <= m < n < length a }
    partition_ a m n i j (ref 0)
    { m <= !j /\ !j < !i /\ !i <= n /\ permut_sub (old a) a m (n+1) /\
      exists x: int.
Andrei Paskevich's avatar
Andrei Paskevich committed
80 81
        (forall r:int. m <= r <= !j -> a[r] <= x) /\
        (forall r:int. !j < r < !i -> a[r] = x) /\
82
        (forall r:int. !i <= r <= n -> a[r] >= x) }
83 84 85 86

end

(*
87
Local Variables:
88
compile-command: "why3ide algo63.mlw"
89
End:
90
*)