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

ObligationsCVC4 1.5
VC max_sum0.05

Theory "vstte10_max_sum.MaxAndSum2": fully verified

ObligationsCVC4 1.5Eprover 2.0
VC max_sum------
split_goal_right
VC max_sum.00.02---
VC max_sum.10.02---
VC max_sum.20.01---
VC max_sum.30.01---
VC max_sum.4------
split_goal_right
VC max_sum.4.00.02---
VC max_sum.4.10.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.10.01---
VC max_sum.50.01---
VC max_sum.60.04---
VC max_sum.70.00---
VC max_sum.80.01---

Theory "vstte10_max_sum.TestCase": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 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.110.02---
VC test.12---0.14
VC test.130.10---
VC test_case---0.00