include "arrays.why"

(***
   	
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   

***)

(* Algorithm 63 *)

parameter partition : 
  a : int array -> m:int -> n:int -> i:int ref -> j:int ref ->
  { m < n } 
  unit writes a,i,j
  { m <= j and j < i and i <= n and permut(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) }