examples/min_max.mlw

   1
   2 (** Computing both the minimum and the maximum of an array of integers
   3
   4     Authors: Jean-Christophe Filliâtre (CNRS)
   5              Guillaume Melquiond       (Inria) *)
   6
   7 use int.Int
   8 use array.Array
   9
  10 (** `m` is the minimum of `a[lo..hi[` *)
  11 predicate is_min (m: int) (a: array int) (lo hi: int) =
  12   (exists i. lo <= i < hi <= length a /\ a[i] = m) /\
  13   (forall i. lo <= i < hi -> m <= a[i])
  14
  15 (** `m` is the maximum of `a[lo..hi[` *)
  16 predicate is_max (m: int) (a: array int) (lo hi: int) =
  17   (exists i. lo <= i < hi <= length a /\ a[i] = m) /\
  18   (forall i. lo <= i < hi -> m >= a[i])
  19
  20 (** first, an obvious implementation *)
  21
  22 let min_max (a: array int) : (int, int)
  23   requires { 1 <= length a }
  24   returns  { x, y -> is_min x a 0 (length a) /\ is_max y a 0 (length a) }
  25 = let ref min = a[0] in
  26   let ref max = a[0] in
  27   for i = 1 to length a - 1 do
  28     invariant { is_min min a 0 i /\ is_max max a 0 i }
  29     if a[i] < min then min <- a[i];
  30     if a[i] > max then max <- a[i]
  31   done;
  32   min, max
  33
  34 (* then a better implementation that considers the values two by two,
  35    to save 25% of comparisons *)
  36
  37 use mach.int.Int
  38 use ref.Refint
  39
  40 let a_better_min_max (a: array int) : (int, int)
  41   requires { 1 <= length a }
  42   returns  { x, y -> is_min x a 0 (length a) /\ is_max y a 0 (length a) }
  43 = [@vc:sp]
  44   let n = length a in
  45   let ref min = a[0] in
  46   let ref max = a[0] in
  47   let ref i = if n % 2 = 0 then 2 else 1 in
  48   if i = 2 then if a[0] < a[1] then max <- a[1] else min <- a[1];
  49   while i < n do
  50     variant   { n - i }
  51     invariant { mod i 2 = mod n 2 }
  52     invariant { is_min min a 0 i /\ is_max max a 0 i }
  53     let x, y = if a[i] < a[i+1] then a[i], a[i+1] else a[i+1], a[i] in
  54     if x < min then min <- x;
  55     if y > max then max <- y;
  56     i += 2
  57   done;
  58   min, max
  59
  60 (** Divide and conqueer is no better, but let's verify it for the fun of it *)
  61
  62 let rec divide_and_conquer (a: array int) (lo hi: int) : (int, int)
  63   requires { 0 <= lo < hi <= length a }
  64   returns  { x, y -> is_min x a lo hi /\ is_max y a lo hi }
  65   variant  { hi - lo }
  66 = if hi - lo = 1 then
  67     a[lo], a[lo]
  68   else if hi - lo = 2 then
  69     if a[lo] < a[lo+1] then a[lo], a[lo+1] else a[lo+1], a[lo]
  70   else
  71     let mid = lo + (hi - lo) / 2 in
  72     let x1, y1 = divide_and_conquer a lo mid in
  73     let x2, y2 = divide_and_conquer a mid hi in
  74     (if x1 < x2 then x1 else x2),
  75     (if y1 > y2 then y1 else y2)
  76
  77 let a_similar_min_max (a: array int) : (int, int)
  78   requires { 1 <= length a }
  79   returns  { x, y -> is_min x a 0 (length a) /\ is_max y a 0 (length a) }
  80 = divide_and_conquer a 0 (length a)