mjrty.mlw 2.42 KB
 Jean-Christophe Filliâtre committed Dec 19, 2011 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 `````` (* 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 from 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 an the extra hypothesis than length a <= max_int) *) module Mjrty use import int.Int use import module ref.Refint use import module array.Array exception Not_found exception Found type candidate type votes = array candidate type param = (M.map int candidate, candidate) predicate pr (p: param) (i: int) = let (m, v) = p in M.([]) m i = v clone import int.NumOfParam with type param = param, predicate pr = pr function numof (a: votes) (c: candidate) (l u: int) : int = num_of (a.elts, c) l u let mjrty (a: votes) = { 1 <= 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 <= i /\ numof a !cand 0 i >= !k /\ 2 * (numof a !cand 0 i - !k) <= i - !k /\ 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; assert { !k = numof a !cand 0 (i+1) }; if 2 * !k > n then raise Found end done; raise Not_found with Found -> !cand end { 2 * numof a result 0 (length a) > length a } | Not_found -> { forall c: candidate. 2 * numof a c 0 (length a) <= length a } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/mjrty.gui" End: *)``````