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

Obligations | Alt-Ergo 2.2.0 | CVC4 1.6 | Z3 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 preservation | 0.46 | --- | --- | |

loop invariant preservation | --- | --- | 0.09 | |

postcondition | 0.26 | --- | --- | |

postcondition | --- | 0.03 | --- | |

out of loop bounds | --- | 0.03 | --- |