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])

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])

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)