algo65.mlw 1.4 KB
Newer Older
1 2

(***
3

4 5
Algorithm 65

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 Algo65

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

22
  (* algorithm 63 *)
23 24

  parameter partition :
25
    a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
26
    { 0 <= m < n < length a }
27
    unit writes a i j
28
    { m <= !j < !i <= n and permut_sub (old a) a m n and
29
      exists x:int.
30 31 32
        (forall r:int. m <= r <= !j -> a[r] <= x) and
        (forall r:int. !j < r < !i -> a[r] = x) and
        (forall r:int. !i <= r <= n -> a[r] >= x) }
33 34 35 36 37 38 39 40 41 42

  (* Algorithm 65 (fixed version) *)

  let rec find (a:array int) (m:int) (n:int) (k:int) : unit variant { n-m } =
    { 0 <= m <= k <= n < length a }
    if m < n then begin
      let i = ref 0 in
      let j = ref 0 in
      label L1:
      partition a m n i j;
43
      assert { permut_sub (at a L1) a m n };
44 45
      label L2:
      if k <= !j then find a m !j k;
46
      assert { permut_sub (at a L2) a m n };
47 48
      if !i <= k then find a !i n k
    end
49
    { permut_sub (old a) a m n and
50 51 52 53 54 55
      (forall r:int. m <= r <= k -> a[r] <= a[k]) and
      (forall r:int. k <= r <= n -> a[k] <= a[r]) }

end

(*
56
Local Variables:
57
compile-command: "unset LANG; make -C ../.. examples/programs/algo65.gui"
58
End:
59
*)