mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
108 lines
2.7 KiB
Plaintext
108 lines
2.7 KiB
Plaintext
|
||
(*
|
||
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
|
||
|
||
See also space_saving.mlw for a related algorithm.
|
||
*)
|
||
|
||
module Candidate
|
||
[@java:package:org.why3.majority]
|
||
[@java:class_kind:interface]
|
||
|
||
type t
|
||
|
||
val equals(self other : t) : bool
|
||
ensures { result <-> self = other }
|
||
end
|
||
|
||
module MjrtyNotFoundException
|
||
[@java:package:org.why3.majority]
|
||
[@java:exception:java.lang.RuntimeException]
|
||
|
||
exception E
|
||
end
|
||
|
||
(*
|
||
module NumOf
|
||
use mach.java.lang.Integer
|
||
use mach.java.lang.Array
|
||
use int.NumOf as N
|
||
|
||
function numof (pr: int -> 'a -> bool) (a: array 'a) (l u: int) : int =
|
||
N.numof (fun i -> pr i a[i]) l u
|
||
end
|
||
|
||
module NumOfEq
|
||
use mach.java.lang.Integer
|
||
use mach.java.lang.Array
|
||
use int.NumOf as N
|
||
|
||
end
|
||
*)
|
||
|
||
module Mjrty
|
||
[@java:package:org.why3.majority]
|
||
|
||
use int.Int
|
||
use ref.Refint
|
||
use int.NumOf as N
|
||
use mach.java.lang.Integer
|
||
use mach.java.lang.Long
|
||
use mach.java.lang.Array
|
||
use Candidate
|
||
use MjrtyNotFoundException
|
||
|
||
function numof (a: array 'a) (v: 'a) (l u: int) : int =
|
||
N.numof (fun i -> a[i] = v) l u
|
||
|
||
let mjrty (a: array Candidate.t) : Candidate.t
|
||
requires { 1 <= length a }
|
||
ensures { 2 * numof a result 0 (length a) > length a }
|
||
raises { MjrtyNotFoundException.E ->
|
||
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:long) 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 equals !cand a[i] then
|
||
k := !k+1
|
||
else
|
||
k := !k-1
|
||
done;
|
||
if !k = 0 then raise MjrtyNotFoundException.E;
|
||
if 2 * !k > Long.of_integer n then return !cand;
|
||
k := 0;
|
||
for i = 0 to n - 1 do
|
||
invariant { !k = numof a !cand 0 i /\ 2 * !k <= n }
|
||
if equals a[i] !cand then begin
|
||
k := !k+1;
|
||
if 2 * !k > Long.of_integer n then return !cand
|
||
end
|
||
done;
|
||
raise MjrtyNotFoundException.E
|
||
|
||
end
|
||
|
||
|