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

(***
   	
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
20
  use import module stdlib.ArrayPermut
21 22 23 24 25 26
 
  (* algorithm 63 *)
 
  parameter partition : 
    a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
    { 0 <= m < n < length a } 
27 28
    unit writes a i j
    { m <= j < i <= n and permut_sub (old a) a m n and
29 30 31 32 33 34 35 36 37 38 39 40 41 42
      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;
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 56 57 58 59
      (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: 
*)