examples/vstte10_max_sum.mlw

   1 (*
   2    VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   3    Problem 1: maximum /\ sum of an array
   4
   5    Author: Jean-Christophe Filliatre (CNRS)
   6    Tool:   Why3 (see http://why3.lri.fr/)
   7 *)
   8
   9 module MaxAndSum
  10
  11   use int.Int
  12   use ref.Ref
  13   use array.Array
  14
  15   let max_sum (a: array int) (n: int) : (sum: int, max: int)
  16     requires { n = length a }
  17     requires { forall i. 0 <= i < n -> a[i] >= 0 }
  18     ensures  { sum <= n * max }
  19   = let ref sum = 0 in
  20     let ref max = 0 in
  21     for i = 0 to n - 1 do
  22       invariant { sum <= i * max }
  23       if max < a[i] then max <- a[i];
  24       sum <- sum + a[i]
  25     done;
  26     sum, max
  27
  28 end
  29
  30 module MaxAndSum2
  31
  32   use int.Int
  33   use ref.Ref
  34   use array.Array
  35   use array.ArraySum
  36
  37   predicate is_max (a: array int) (l h: int) (m: int) =
  38     (forall k. l <= k < h -> a[k] <= m) &&
  39     ((h <= l && m = 0) ||
  40      (l <  h && exists k. l <= k < h && m = a[k]))
  41
  42   let max_sum (a: array int) (n: int) : (s: int, m: int)
  43     requires { n = length a /\ forall i. 0 <= i < n -> a[i] >= 0 }
  44     ensures  { s = sum a 0 n /\ is_max a 0 n m /\ s <= n * m }
  45   = let ref s = 0 in
  46     let ref m = 0 in
  47     for i = 0 to n - 1 do
  48       invariant { s = sum a 0 i }
  49       invariant { is_max a 0 i m }
  50       invariant { s <= i * m }
  51       if m < a[i] then m <- a[i];
  52       s <- s + a[i]
  53     done;
  54     s, m
  55
  56 end
  57
  58 module TestCase
  59
  60   use int.Int
  61   use MaxAndSum2
  62   use array.Array
  63   use array.ArraySum
  64
  65   exception BenchFailure
  66
  67   let test () =
  68     let n = 10 in
  69     let a = make n 0 in
  70     a[0] <- 9;
  71     a[1] <- 5;
  72     a[2] <- 0;
  73     a[3] <- 2;
  74     a[4] <- 7;
  75     a[5] <- 3;
  76     a[6] <- 2;
  77     a[7] <- 1;
  78     a[8] <- 10;
  79     a[9] <- 6;
  80     let s, m = max_sum a n in
  81     assert { s = 45 };
  82     assert { m = 10 };
  83     s, m
  84
  85   let test_case () raises { BenchFailure -> true } =
  86     let s, m = test () in
  87     (* bench of --exec *)
  88     if s <> 45  then raise BenchFailure;
  89     if m <> 10  then raise BenchFailure;
  90     s,m
  91
  92 end