Wiki Agenda Contact Version française

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

ObligationsCVC4 1.5
VC for max_sum0.05

Theory "vstte10_max_sum.MaxAndSum2": fully verified

ObligationsAlt-Ergo 2.3.0Eprover 2.0
VC for max_sum------
split_vc
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.01---
index in array bounds0.01---
index in array bounds0.01---
index in array bounds0.01---
loop invariant preservation0.02---
loop invariant preservation0.06---
loop invariant preservation------
assert (s1 <= i * m)
asserted formula------
assert (i * m1 <= i * m)
asserted formula---3.55
asserted formula0.01---
loop invariant preservation0.01---
index in array bounds0.00---
loop invariant preservation0.01---
loop invariant preservation0.08---
loop invariant preservation0.01---
postcondition0.00---
VC for max_sum0.00---

Theory "vstte10_max_sum.TestCase": fully verified

ObligationsAlt-Ergo 2.0.0Alt-Ergo 2.3.0CVC4 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 bounds0.02------
index in array bounds------0.02
index in array bounds0.10------
precondition------0.02
assertion------0.63
assertion---0.16---
VC for test_case---0.00---