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