(**********************************************************************)
(*                                                                    *)
(* FIND, an historical example.                                       *)
(*                                                                    *)
(* The proof of this program was originally done by C. A. R. Hoare    *)
(* and fully detailed in the following paper:                         *)
(*                                                                    *)
(* C. A. R. Hoare, "Proof of a Program: FIND", Communications of the  *)
(* ACM, 14(1), 39--45, January 1971.                                  *)
(*                                                                    *)
(**********************************************************************)
(* Jean-Christophe FILLIATRE, February 98                             *)
(**********************************************************************)

include "arrays.why"

(* specification *)

logic N : int
logic f : int

axiom f_N_range : 1 <= f <= N

predicate found(A : int farray) =
  forall p,q:int. 1 <= p <= f <= q <= N -> A[p] <= A[f] <= A[q]

predicate m_invariant(m : int, A : int farray) =
  m <= f and forall p,q:int. 1 <= p < m <= q <= N -> A[p] <= A[q]

predicate n_invariant(n : int, A : int farray) =
  f <= n and forall p,q:int. 1 <= p <= n < q <= N -> A[p] <= A[q]

predicate i_invariant(m : int, n : int, i : int, r : int, A : int farray) =
  m <= i and (forall p:int. 1 <= p < i -> A[p] <= r) and
  (i <= n -> exists p:int. i <= p <= n and r <= A[p])

predicate j_invariant(m : int, n : int, j : int, r : int, A : int farray) =
  j <= n and (forall q:int. j < q <= N -> r <= A[q]) and
  (m <= j -> exists q:int. m <= q <= j and A[q] <= r)

predicate termination(i:int, j:int, i0:int, j0:int, r:int, A:int farray) =
  (i > i0 and j < j0) or (i <= f <= j and A[f] = r)

(* Implementation part *)

parameter A : int array (* the array *)

let find () =
  { array_length(A) = N+1 }
  init:
  let m = ref 1 in let n = ref N in
  while !m < !n do
    { invariant m_invariant(m,A) and n_invariant(n,A) and permutation(A,A@init) 
             and 1 <= m and n <= N as Inv_mn
      variant n-m }
    let r = A[f] in let i = ref !m in let j = ref !n in 
    begin
      while !i <= !j do
        { invariant i_invariant(m,n,i,r,A) and j_invariant(m,n,j,r,A)
      	         and m_invariant(m,A) and n_invariant(n,A)
		 and 0 <= j and i <= N+1
		 and termination(i,j,m,n,r,A)
      	       	 and permutation(A,A@init) as Inv_ij
          variant N+2+j-i }
        L:

        while A[!i] < r do
          { invariant i_invariant(m, n, i, r, A) 
      	       	   and i@L <= i and i <= n
		   and termination(i, j, m, n, r, A) as Inv_i
      	    variant N+1-i }
          i := !i + 1
        done;
      	
        while r < A[!j] do
          { invariant j_invariant(m, n, j, r, A) 
      	       	   and j <= j@L and m <= j
		   and termination(i, j, m, n, r, A) as Inv_j
            variant j }
       	  j := !j - 1
        done;

        assert { A[j] <= r and r <= A[i] };

        if !i <= !j then begin
          let w = A[!i] in begin A[!i] := A[!j]; A[!j] := w end;
	  assert { exchange(A, A@L, i, j) };
	  assert { A[i] <= r }; assert { r <= A[j] };
	  i := !i + 1;
	  j := !j - 1
        end
      done;

      assert { m < i and j < n };

      if f <= !j then
        n := !j
      else if !i <= f then
        m := !i
      else
        begin n := f; m := f end
    end
  done
  { found(A) and permutation(A,A@) }