## Sum and Maximum, in Why3

Sum and Maximum of an array of integers, in Why3

Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure

Tools: 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 sum = ref 0 in
let max = ref 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: int. l <= k < h -> a[k] <= m) &&
((h <= l && m = 0) ||
(l <  h && exists k: int. l <= k < h && m = a[k]))

let max_sum (a: array int) (n: int)
requires { n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
ensures  { let s, m = result in
s = sum a 0 n /\ is_max a 0 n m /\ s <= n * m }
= let s = ref 0 in
let m = ref 0 in
for i = 0 to n - 1 do
invariant { !s = sum a 0 i /\ is_max a 0 i !m /\ !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 max_sum 0.05

## Theory "vstte10_max_sum.MaxAndSum2": fully verified

 Obligations CVC4 1.5 Eprover 2.0 VC max_sum --- --- split_goal_right VC max_sum.0 0.02 --- VC max_sum.1 0.02 --- VC max_sum.2 0.01 --- VC max_sum.3 0.01 --- VC max_sum.4 --- --- split_goal_right VC max_sum.4.0 0.02 --- VC max_sum.4.1 0.02 --- VC max_sum.4.2 --- --- introduce_premises VC max_sum.4.2.0 --- --- assert (i*m1 <= i * m) VC max_sum.4.2.0.0 --- 0.02 VC max_sum.4.2.0.1 0.01 --- VC max_sum.5 0.01 --- VC max_sum.6 0.04 --- VC max_sum.7 0.00 --- VC max_sum.8 0.01 ---

## Theory "vstte10_max_sum.TestCase": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.5 VC test --- --- split_goal_right VC test.0 --- 0.00 VC test.1 --- 0.01 VC test.2 --- 0.02 VC test.3 --- 0.01 VC test.4 --- 0.01 VC test.5 --- 0.01 VC test.6 --- 0.01 VC test.7 --- 0.02 VC test.8 --- 0.02 VC test.9 --- 0.02 VC test.10 --- 0.02 VC test.11 0.02 --- VC test.12 --- 0.14 VC test.13 0.10 --- VC test_case --- 0.00