algo65.mlw 1.42 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26

(***
   	
Algorithm 65

C. A. R. Hoare 	 
Elliott Brothers Ltd., Hertfordshire, England, U.K.

Communications of the ACM  archive
Volume 4 ,  Issue 7  (July 1961) table of contents
Pages: 321 - 322   

***)

module Algo65

  use import int.Int
  use import module stdlib.Ref
  use import module stdlib.Array
  use import array.ArrayPermut
 
  (* algorithm 63 *)
 
  parameter partition : 
    a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
    { 0 <= m < n < length a } 
27
    unit writes a.contents i.contents j.contents
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
    { m <= j < i <= n and permut (old a) a m n and
      exists x:int.
        (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) }

  (* 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;
      assert { permut (at a L1) a m n };
      label L2:
      if k <= !j then find a m !j k;
      assert { permut (at a L2) a m n };
      if !i <= k then find a !i n k
    end
    { permut (old a) a m n and 
      (forall r:int. m <= r <= k -> a[r] <= a[k]) and
      (forall r:int. k <= r <= n -> a[k] <= a[r]) }

end

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