## 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 import int.Int
use import ref.Ref
use import array.Array

let max_sum (a: array int) (n: int)
requires { n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
ensures { let (sum, max) = result in 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 import int.Int
use import ref.Ref
use import array.Array
use import 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 import MaxAndSum2
use import array.Array
use import 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 in 0.00 s

 Obligations Alt-Ergo (0.99.1) CVC3 (2.4.1) Coq (8.6.1) 1. VC for max_sum --- --- --- split_goal_wp 1. postcondition 0.00 0.00 --- 2. loop invariant init 0.00 0.00 --- 3. index in array bounds 0.00 --- --- 4. index in array bounds 0.00 --- --- 5. index in array bounds 0.00 --- --- 6. loop invariant preservation --- --- 0.29 7. index in array bounds 0.01 --- --- 8. loop invariant preservation 0.00 --- --- 9. postcondition 0.01 0.01 ---

## Theory "vstte10_max_sum.MaxAndSum2": fully verified in 0.00 s

 Obligations Alt-Ergo (0.99.1) CVC3 (2.4.1) Coq (8.6.1) Z3 (3.2) 1. VC for max_sum --- --- --- --- split_goal_wp 1. postcondition 0.01 0.01 --- --- 2. loop invariant init 0.01 0.01 --- --- 3. index in array bounds 0.01 --- --- --- 4. index in array bounds 0.00 --- --- --- 5. index in array bounds 0.01 --- --- --- 6. loop invariant preservation --- --- --- --- split_goal_wp 1. VC for max_sum 0.02 --- --- --- 2. VC for max_sum --- --- --- 0.02 3. VC for max_sum --- --- 0.30 --- 7. index in array bounds 0.02 --- --- --- 8. loop invariant preservation --- --- --- --- split_goal_wp 1. VC for max_sum 0.02 --- --- --- 2. VC for max_sum 0.04 0.04 --- --- 3. VC for max_sum 0.01 --- --- --- 9. postcondition 0.00 0.01 --- ---

## Theory "vstte10_max_sum.TestCase": fully verified in 0.04 s

 Obligations Alt-Ergo (0.99.1) CVC3 (2.4.1) CVC4 (1.4) Z3 (3.2) Z3 (4.3.2) 1. VC for test --- --- --- --- --- split_goal_wp 1. array creation size 0.02 0.00 0.00 --- 0.01 2. index in array bounds 0.00 0.00 0.00 --- 0.02 3. index in array bounds 0.01 0.01 0.01 --- 0.01 4. index in array bounds 0.01 0.01 0.00 --- 0.01 5. index in array bounds 0.02 0.01 0.00 --- 0.01 6. index in array bounds 0.02 0.01 0.00 --- 0.01 7. index in array bounds 0.02 0.01 0.01 --- 0.01 8. index in array bounds 0.01 0.01 0.01 --- 0.01 9. index in array bounds 0.03 0.01 0.00 --- 0.01 10. index in array bounds 0.03 0.01 0.01 --- 0.01 11. index in array bounds 0.03 0.01 0.01 --- 0.01 12. precondition 0.09 0.02 0.02 --- 0.01 13. assertion --- 0.10 0.14 --- 0.02 14. assertion 0.22 --- --- --- 0.04 2. VC for test_case 0.02 0.01 0.01 0.00 0.00