(*
   Boyer and Moore’s MJRTY algorithm (1980)
   Determines the majority, if any, of a multiset of n votes.
   Uses at most 2n comparisons and constant extra space (3 variables).

   MJRTY - A Fast Majority Vote Algorithm.
   Robert S. Boyer, J Strother Moore.
   In R.S. Boyer (ed.), Automated Reasoning: Essays in Honor of Woody
   Bledsoe, Automated Reasoning Series, Kluwer Academic Publishers,
   Dordrecht, The Netherlands, 1991, pp. 105-117.

   http://www.cs.utexas.edu/users/boyer/mjrty.ps.Z

   Changes w.r.t. the article above:
   - arrays are 0-based
   - we assume the input array to have at least one element
   - we use 2x <= y instead of x <= floor(y/2), which is equivalent

   See also space_saving.mlw for a related algorithm.
*)

module Mjrty

  use int.Int
  use ref.Refint
  use array.Array
  use array.NumOfEq

  exception Not_found

  type candidate

  val (=) (x y: candidate) : bool
    ensures { result <-> x = y }

  let mjrty (a: array candidate) : candidate
    requires { 1 <= length a }
    ensures  { 2 * numof a result 0 (length a) > length a }
    raises   { Not_found -> forall c. 2 * numof a c 0 (length a) <= length a }
  = let n = length a in
    let cand = ref a[0] in
    let k = ref 0 in
    for i = 0 to n - 1 do (* could start at 1 with k initialized to 1 *)
      invariant { 0 <= !k <= numof a !cand 0 i }
      invariant { 2 * (numof a !cand 0 i - !k) <= i - !k }
      invariant { forall c. c <> !cand -> 2 * numof a c 0 i <= i - !k }
      if !k = 0 then begin
        cand := a[i];
        k := 1
      end else if !cand = a[i] then
        incr k
      else
        decr k
    done;
    if !k = 0 then raise Not_found;
    if 2 * !k > n then return !cand;
    k := 0;
    for i = 0 to n - 1 do
      invariant { !k = numof a !cand 0 i /\ 2 * !k <= n }
      if a[i] = !cand then begin
        incr k;
        if 2 * !k > n then return !cand
      end
    done;
    raise Not_found

end