(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 1: maximum /\ sum of an array

   Author: Jean-Christophe Filliatre (CNRS)
   Tool:   Why3 (see http://why3.lri.fr/)
*)

module MaxAndSum

  use int.Int
  use ref.Ref
  use array.Array

  let max_sum (a: array int) (n: int) : (sum: int, max: int)
    requires { n = length a }
    requires { forall i. 0 <= i < n -> a[i] >= 0 }
    ensures  { sum <= n * max }
  = let ref sum = 0 in
    let ref max = 0 in
    for i = 0 to n - 1 do
      invariant { sum <= i * max }
      if max < a[i] then max <- a[i];
      sum <- sum + a[i]
    done;
    sum, max

end

module MaxAndSum2

  use int.Int
  use ref.Ref
  use array.Array
  use array.ArraySum

  predicate is_max (a: array int) (l h: int) (m: int) =
    (forall k. l <= k < h -> a[k] <= m) &&
    ((h <= l && m = 0) ||
     (l <  h && exists k. l <= k < h && m = a[k]))

  let max_sum (a: array int) (n: int) : (s: int, m: int)
    requires { n = length a /\ forall i. 0 <= i < n -> a[i] >= 0 }
    ensures  { s = sum a 0 n /\ is_max a 0 n m /\ s <= n * m }
  = let ref s = 0 in
    let ref m = 0 in
    for i = 0 to n - 1 do
      invariant { s = sum a 0 i }
      invariant { is_max a 0 i m }
      invariant { s <= i * m }
      if m < a[i] then m <- a[i];
      s <- s + a[i]
    done;
    s, m

end

module TestCase

  use int.Int
  use MaxAndSum2
  use array.Array
  use array.ArraySum

  exception BenchFailure

  let test () =
    let n = 10 in
    let a = make n 0 in
    a[0] <- 9;
    a[1] <- 5;
    a[2] <- 0;
    a[3] <- 2;
    a[4] <- 7;
    a[5] <- 3;
    a[6] <- 2;
    a[7] <- 1;
    a[8] <- 10;
    a[9] <- 6;
    let s, m = max_sum a n in
    assert { s = 45 };
    assert { m = 10 };
    s, m

  let test_case () raises { BenchFailure -> true } =
    let s, m = test () in
    (* bench of --exec *)
    if s <> 45  then raise BenchFailure;
    if m <> 10  then raise BenchFailure;
    s,m

end