Wiki Agenda Contact Version française

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


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Historical examples

Tools: 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
   - we do not consider arithmetic overflows (easy, but requires the
     extra hypothesis length a <= max_int)
*)

module Mjrty

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

  exception Not_found
  exception Found

  type candidate

  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: candidate. 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:candidate. 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;
    try
      if 2 * !k > n then raise Found;
      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 raise Found
        end
      done;
      raise Not_found
    with Found ->
      !cand
    end

end

download ZIP archive

Why3 Proof Results for Project "mjrty"

Theory "mjrty.Mjrty": fully verified in 3.43 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Z3 (4.3.2)
VC for mjrty------------
split_goal_wp
  1. index in array bounds0.01---------
2. exceptional postcondition0.02---------
3. loop invariant init0.02---------
4. loop invariant init0.02---------
5. loop invariant init0.02---------
6. index in array bounds0.00---------
7. loop invariant preservation0.05---------
8. loop invariant preservation------1.400.01
9. loop invariant preservation---0.22------
10. index in array bounds0.00---------
11. loop invariant preservation0.03---------
12. loop invariant preservation0.08---------
13. loop invariant preservation---0.14------
14. loop invariant preservation0.05---------
15. loop invariant preservation---0.04------
16. loop invariant preservation---0.35------
17. exceptional postcondition0.00---------
18. postcondition---------0.02
19. exceptional postcondition0.03---------
20. loop invariant init0.01---------
21. index in array bounds0.02---------
22. postcondition------0.77---
23. loop invariant preservation0.07---------
24. loop invariant preservation---0.04------
25. exceptional postcondition0.01---------