algo65.mlw 1.75 KB
Newer Older
1
(***
2

3 4
Algorithm 65

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

***)

module Algo65

16 17 18 19
  use int.Int
  use ref.Ref
  use array.Array
  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 28
    ensures  { m <= !j < !i <= n }
    ensures  { permut_sub (old a) a m (n+1) }
29 30 31
    ensures  { forall r:int. m <= r <= !j -> a[r] <= !x }
    ensures  { forall r:int. !j < r < !i -> a[r] = !x }
    ensures  { forall r:int. !i <= r <= n -> a[r] >= !x }
32 33 34

  (* Algorithm 65 (fixed version) *)

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 39 40
    ensures  { permut_sub (old a) a m (n+1) }
    ensures  { forall r:int. m <= r <= k -> a[r] <= a[k] }
    ensures  { forall r:int. k <= r <= n -> a[k] <= a[r] }
41
  = if m < n then begin
42 43
      let i = ref 0 in
      let j = ref 0 in
44 45
      let ghost x = ref 42 in
      partition a m n i j x;
46
    label L1 in
47
      if k <= !j then find a m !j k;
48 49
      assert { permut_sub (a at L1) a m (n+1) };
      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 56
      assert { permut_sub (a at L2) a m (n+1) };
      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 61 62
    end

end