(***

Algorithm 63

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 Algo63

  use import int.Int
  use import module ref.Ref
  use import module array.Array
  use import module array.ArrayPermut

  val partition :
    a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
    { m < n }
    unit writes a i j
    { m <= !j /\ !j < !i /\ !i <= n /\ permut_sub (old a) a m n /\
      exists x:int.
        (forall r:int. m <= r <= !j -> a[r] <= x) /\
        (forall r:int. !j < r < !i -> a[r] = x) /\
        (forall r:int. !i <= r <= n -> a[r] >= x) }

end

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