## Sum and Maximum, in Why3

Sum and Maximum of an array of integers, in Why3

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure

Outils: Why3

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

```(*
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
```

# Why3 Proof Results for Project "vstte10_max_sum"

## Theory "vstte10_max_sum.MaxAndSum": fully verified

 Obligations CVC4 1.5 VC for max_sum 0.05

## Theory "vstte10_max_sum.MaxAndSum2": fully verified

 Obligations Alt-Ergo 2.3.0 Eprover 2.0 VC for max_sum --- --- split_vc loop invariant init 0.01 --- loop invariant init 0.01 --- loop invariant init 0.01 --- index in array bounds 0.01 --- index in array bounds 0.01 --- index in array bounds 0.01 --- loop invariant preservation 0.02 --- loop invariant preservation 0.06 --- loop invariant preservation --- --- assert (s1 <= i * m) asserted formula --- --- assert (i * m1 <= i * m) asserted formula --- 3.48 asserted formula 0.01 --- loop invariant preservation 0.01 --- index in array bounds 0.00 --- loop invariant preservation 0.01 --- loop invariant preservation 0.08 --- loop invariant preservation 0.01 --- postcondition 0.00 --- VC for max_sum 0.00 ---

## Theory "vstte10_max_sum.TestCase": fully verified

 Obligations Alt-Ergo 2.1.0 Alt-Ergo 2.3.0 CVC4 1.5 VC for test --- --- --- split_goal_right array creation size --- --- 0.01 index in array bounds --- --- 0.00 index in array bounds --- --- 0.01 index in array bounds --- --- 0.02 index in array bounds --- --- 0.02 index in array bounds --- --- 0.01 index in array bounds --- --- 0.02 index in array bounds --- --- 0.02 index in array bounds 0.02 --- --- index in array bounds --- --- 0.02 index in array bounds 0.10 --- --- precondition --- --- 0.02 assertion --- --- 0.63 assertion --- 0.16 --- VC for test_case --- 0.00 ---