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 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.83 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)Coq (8.4pl6)
VC for max_sum---------
split_goal_wp
  1. postcondition0.000.00---
2. loop invariant init0.000.00---
3. index in array bounds0.00------
4. index in array bounds0.00------
5. index in array bounds0.00------
6. loop invariant preservation------0.80
7. index in array bounds0.01------
8. loop invariant preservation0.00------
9. postcondition0.010.01---

Theory "vstte10_max_sum.MaxAndSum2": fully verified in 1.07 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)Coq (8.4pl6)Z3 (3.2)
VC for max_sum------------
split_goal_wp
  1. postcondition0.010.01------
2. loop invariant init0.010.01------
3. index in array bounds0.01---------
4. index in array bounds0.00---------
5. index in array bounds0.01---------
6. loop invariant preservation------------
split_goal_wp
  1. VC for max_sum0.02---------
2. VC for max_sum---------0.02
3. VC for max_sum------0.83---
7. index in array bounds0.02---------
8. loop invariant preservation------------
split_goal_wp
  1. VC for max_sum0.02---------
2. VC for max_sum0.040.04------
3. VC for max_sum0.01---------
9. postcondition0.000.01------

Theory "vstte10_max_sum.TestCase": fully verified in 1.16 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Z3 (3.2)Z3 (4.3.2)
VC for test---------------
split_goal_wp
  1. array creation size0.020.000.00---0.01
2. index in array bounds0.000.000.00---0.02
3. index in array bounds0.010.010.01---0.01
4. index in array bounds0.010.010.00---0.01
5. index in array bounds0.020.010.00---0.01
6. index in array bounds0.020.010.00---0.01
7. index in array bounds0.020.010.01---0.01
8. index in array bounds0.010.010.01---0.01
9. index in array bounds0.030.010.00---0.01
10. index in array bounds0.030.010.01---0.01
11. index in array bounds0.030.010.01---0.01
12. precondition0.090.020.02---0.01
13. assertion---0.100.14---0.02
14. assertion0.22---------0.04
VC for test_case0.020.010.010.000.00