mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
81 lines
2.5 KiB
Plaintext
81 lines
2.5 KiB
Plaintext
|
|
(** 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
|
|
|
|
(** `m` is the minimum of `a[lo..hi[` *)
|
|
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 maximum 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])
|
|
|
|
(** 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)
|