examples/mjrty.mlw

   1
   2 (*
   3    Boyer and Moore’s MJRTY algorithm (1980)
   4    Determines the majority, if any, of a multiset of n votes.
   5    Uses at most 2n comparisons and constant extra space (3 variables).
   6
   7    MJRTY - A Fast Majority Vote Algorithm.
   8    Robert S. Boyer, J Strother Moore.
   9    In R.S. Boyer (ed.), Automated Reasoning: Essays in Honor of Woody
  10    Bledsoe, Automated Reasoning Series, Kluwer Academic Publishers,
  11    Dordrecht, The Netherlands, 1991, pp. 105-117.
  12
  13    http://www.cs.utexas.edu/users/boyer/mjrty.ps.Z
  14
  15    Changes w.r.t. the article above:
  16    - arrays are 0-based
  17    - we assume the input array to have at least one element
  18    - we use 2x <= y instead of x <= floor(y/2), which is equivalent
  19
  20    See also space_saving.mlw for a related algorithm.
  21 *)
  22
  23 module Mjrty
  24
  25   use int.Int
  26   use ref.Refint
  27   use array.Array
  28   use array.NumOfEq
  29
  30   exception Not_found
  31
  32   type candidate
  33
  34   val (=) (x y: candidate) : bool
  35     ensures { result <-> x = y }
  36
  37   let mjrty (a: array candidate) : candidate
  38     requires { 1 <= length a }
  39     ensures  { 2 * numof a result 0 (length a) > length a }
  40     raises   { Not_found -> forall c. 2 * numof a c 0 (length a) <= length a }
  41   = let n = length a in
  42     let cand = ref a[0] in
  43     let k = ref 0 in
  44     for i = 0 to n - 1 do (* could start at 1 with k initialized to 1 *)
  45       invariant { 0 <= !k <= numof a !cand 0 i }
  46       invariant { 2 * (numof a !cand 0 i - !k) <= i - !k }
  47       invariant { forall c. c <> !cand -> 2 * numof a c 0 i <= i - !k }
  48       if !k = 0 then begin
  49         cand := a[i];
  50         k := 1
  51       end else if !cand = a[i] then
  52         incr k
  53       else
  54         decr k
  55     done;
  56     if !k = 0 then raise Not_found;
  57     if 2 * !k > n then return !cand;
  58     k := 0;
  59     for i = 0 to n - 1 do
  60       invariant { !k = numof a !cand 0 i /\ 2 * !k <= n }
  61       if a[i] = !cand then begin
  62         incr k;
  63         if 2 * !k > n then return !cand
  64       end
  65     done;
  66     raise Not_found
  67
  68 end