(*** 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 ref.Ref use import module array.Array use import module array.ArrayPermut (* algorithm 63 *) parameter partition : a : array int -> m:int -> n:int -> i:ref int -> j:ref int -> { 0 <= m < n < length a } unit writes a i j { m <= j < i <= n and permut_sub (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_sub (at a L1) a m n }; label L2: if k <= !j then find a m !j k; assert { permut_sub (at a L2) a m n }; if !i <= k then find a !i n k end { permut_sub (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: *)