Wiki Agenda Contact Version française

Most Frequent Value in a Sorted Array

Search for the most frequent value in a sorted array, in constant space.


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


A simple programming exercise: find out the most frequent value in an array

Using an external table (e.g. a hash table), we can easily do it in linear time and space.

However, if the array is sorted, we can do it in linear time and constant space.

Author: Jean-Christophe FilliĆ¢tre (CNRS)

use int.Int
use ref.Refint
use array.Array
use array.NumOfEq

let most_frequent (a: array int) : int
  requires { length a > 0 }
  requires { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
  ensures  { numof a result 0 (length a) > 0 }
  ensures  { forall x. numof a x 0 (length a) <= numof a result 0 (length a) }
= let ref r = a[0] in
  let ref c = 1 in
  let ref m = 1 in
  for i = 1 to length a - 1 do
    invariant { c = numof a a[i-1] 0 i }
    invariant { m = numof a r 0 i }
    invariant { forall x. numof a x 0 i <= m }
    if a[i] = a[i-1] then begin
      incr c;
      if c > m then begin m <- c; r <- a[i] end
    end else
      c <- 1
  done;
  r

download ZIP archive

Why3 Proof Results for Project "array_most_frequent"

Theory "array_most_frequent.Top": fully verified

ObligationsAlt-Ergo 2.2.0CVC4 1.6Z3 4.6.0
VC for most_frequent---------
split_vc
index in array bounds---0.03---
loop invariant init---0.04---
loop invariant init---0.03---
loop invariant init---0.04---
index in array bounds---0.04---
index in array bounds---0.03---
index in array bounds---0.03---
loop invariant preservation---0.07---
loop invariant preservation---0.03---
loop invariant preservation---0.17---
loop invariant preservation---0.07---
loop invariant preservation---0.06---
loop invariant preservation---0.29---
loop invariant preservation------0.03
loop invariant preservation0.46------
loop invariant preservation------0.09
postcondition0.26------
postcondition---0.03---
out of loop bounds---0.03---