## 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

**References:** The 1st Verified Software Competition / The VerifyThis Benchmarks

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

download ZIP archive

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

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.0.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 | --- |