Find all necessary invariants (A,B,C,D) for a proof of (partial) correctness of the following program.  The program places the kth largest element of an array S[1:N], N>0, of reals in position k.  In the process it rearranges the array.

(m,n) := (1,N)
while {A:} m < n do
   (i,j,r) := (m,n,S[k])
    while{B:} i < j do
       while {C:} S[i] < r do i := i+1
      while {D:} r < S[j] do j := j-1
      if i < j then
            (S[i],S[j],i,j) := (S[j],S[i],i+1,j-1)
    if k < j then n := j
    else if i < k then m := i
    else (m,n) := (k,k)