## 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).

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure / Historical examples

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

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