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

Obligations | Alt-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 bounds | 0.01 | --- | --- | --- | |

2. exceptional postcondition | 0.02 | --- | --- | --- | |

3. loop invariant init | 0.02 | --- | --- | --- | |

4. loop invariant init | 0.02 | --- | --- | --- | |

5. loop invariant init | 0.02 | --- | --- | --- | |

6. index in array bounds | 0.00 | --- | --- | --- | |

7. loop invariant preservation | 0.05 | --- | --- | --- | |

8. loop invariant preservation | --- | --- | 1.40 | 0.01 | |

9. loop invariant preservation | --- | 0.22 | --- | --- | |

10. index in array bounds | 0.00 | --- | --- | --- | |

11. loop invariant preservation | 0.03 | --- | --- | --- | |

12. loop invariant preservation | 0.08 | --- | --- | --- | |

13. loop invariant preservation | --- | 0.14 | --- | --- | |

14. loop invariant preservation | 0.05 | --- | --- | --- | |

15. loop invariant preservation | --- | 0.04 | --- | --- | |

16. loop invariant preservation | --- | 0.35 | --- | --- | |

17. exceptional postcondition | 0.00 | --- | --- | --- | |

18. postcondition | --- | --- | --- | 0.02 | |

19. exceptional postcondition | 0.03 | --- | --- | --- | |

20. loop invariant init | 0.01 | --- | --- | --- | |

21. index in array bounds | 0.02 | --- | --- | --- | |

22. postcondition | --- | --- | 0.77 | --- | |

23. loop invariant preservation | 0.07 | --- | --- | --- | |

24. loop invariant preservation | --- | 0.04 | --- | --- | |

25. exceptional postcondition | 0.01 | --- | --- | --- |