## Minimum and maximum of an array of integers

Various ways of computing both the minimum and the maximum of an array of integers

Topics: Array Data Structure / Algorithms

Tools: Why3

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

Computing both the minimum and the maximum of an array of integers

Authors: Jean-Christophe FilliĆ¢tre (CNRS) Guillaume Melquiond (Inria)

```use int.Int
use array.Array

predicate is_min (m: int) (a: array int) (lo hi: int) =
(exists i. lo <= i < hi <= length a /\ a[i] = m) /\
(forall i. lo <= i < hi -> m <= a[i])
```

`m` is the minimum of `a[lo..hi[`

```predicate is_max (m: int) (a: array int) (lo hi: int) =
(exists i. lo <= i < hi <= length a /\ a[i] = m) /\
(forall i. lo <= i < hi -> m >= a[i])
```

`m` is the maximum of `a[lo..hi[`

first, an obvious implementation

```let min_max (a: array int) : (int, int)
requires { 1 <= length a }
returns  { x, y -> is_min x a 0 (length a) /\ is_max y a 0 (length a) }
= let ref min = a[0] in
let ref max = a[0] in
for i = 1 to length a - 1 do
invariant { is_min min a 0 i /\ is_max max a 0 i }
if a[i] < min then min <- a[i];
if a[i] > max then max <- a[i]
done;
min, max

(* then a better implementation that considers the values two by two,
to save 25% of comparisons *)

use mach.int.Int
use ref.Refint

let a_better_min_max (a: array int) : (int, int)
requires { 1 <= length a }
returns  { x, y -> is_min x a 0 (length a) /\ is_max y a 0 (length a) }
= [@vc:sp]
let n = length a in
let ref min = a[0] in
let ref max = a[0] in
let ref i = if n % 2 = 0 then 2 else 1 in
if i = 2 then if a[0] < a[1] then max <- a[1] else min <- a[1];
while i < n do
variant   { n - i }
invariant { mod i 2 = mod n 2 }
invariant { is_min min a 0 i /\ is_max max a 0 i }
let x, y = if a[i] < a[i+1] then a[i], a[i+1] else a[i+1], a[i] in
if x < min then min <- x;
if y > max then max <- y;
i += 2
done;
min, max

```

Divide and conqueer is no better, but let's verify it for the fun of it

```let rec divide_and_conquer (a: array int) (lo hi: int) : (int, int)
requires { 0 <= lo < hi <= length a }
returns  { x, y -> is_min x a lo hi /\ is_max y a lo hi }
variant  { hi - lo }
= if hi - lo = 1 then
a[lo], a[lo]
else if hi - lo = 2 then
if a[lo] < a[lo+1] then a[lo], a[lo+1] else a[lo+1], a[lo]
else
let mid = lo + (hi - lo) / 2 in
let x1, y1 = divide_and_conquer a lo mid in
let x2, y2 = divide_and_conquer a mid hi in
(if x1 < x2 then x1 else x2),
(if y1 > y2 then y1 else y2)

let a_similar_min_max (a: array int) : (int, int)
requires { 1 <= length a }
returns  { x, y -> is_min x a 0 (length a) /\ is_max y a 0 (length a) }
= divide_and_conquer a 0 (length a)
```