mjrty.mlw 1.84 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14

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

15
   Changes w.r.t. the article above:
16 17 18
   - 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
19

20 21 22 23
*)

module Mjrty

24 25 26 27
  use int.Int
  use ref.Refint
  use array.Array
  use array.NumOfEq
28 29 30 31 32

  exception Not_found

  type candidate

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

36
  let mjrty (a: array candidate) : candidate
37 38
    requires { 1 <= length a }
    ensures  { 2 * numof a result 0 (length a) > length a }
39
    raises   { Not_found -> forall c. 2 * numof a c 0 (length a) <= length a }
40
  = let n = length a in
41 42
    let cand = ref a[0] in
    let k = ref 0 in
43
    for i = 0 to n - 1 do (* could start at 1 with k initialized to 1 *)
44
      invariant { 0 <= !k <= numof a !cand 0 i }
45 46
      invariant { 2 * (numof a !cand 0 i - !k) <= i - !k }
      invariant { forall c. c <> !cand -> 2 * numof a c 0 i <= i - !k }
47 48 49
      if !k = 0 then begin
        cand := a[i];
        k := 1
50
      end else if !cand = a[i] then
51 52 53 54 55
        incr k
      else
        decr k
    done;
    if !k = 0 then raise Not_found;
56 57
    if 2 * !k > n then return !cand;
    k := 0;
58
    for i = 0 to n - 1 do
59
      invariant { !k = numof a !cand 0 i /\ 2 * !k <= n }
60
      if a[i] = !cand then begin
61 62 63 64 65
        incr k;
        if 2 * !k > n then return !cand
      end
    done;
    raise Not_found
66 67

end