1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function Sum(a: seq<int>, s: int, t: int): int
requires 0 <= s <= t <= |a|;
{
if s == t then 0 else Sum(a, s, t-1) + a[t-1]
}
method MaxSegSum(a: seq<int>) returns (k: int, m: int)
ensures 0 <= k <= m <= |a|;
ensures forall p,q :: 0 <= p <= q <= |a| ==> Sum(a, p, q) <= Sum(a, k, m);
{
k, m := 0, 0;
var s := 0; // invariant s == Sum(a, k, m)
var n := 0;
var c, t := 0, 0; // invariant t == Sum(a, c, n)
while (n < |a|)
invariant n <= |a|;
invariant 0 <= c <= n && t == Sum(a, c, n);
invariant forall b :: 0 <= b <= n ==> Sum(a, b, n) <= Sum(a, c, n);
invariant 0 <= k <= m <= n && s == Sum(a, k, m);
invariant forall p,q :: 0 <= p <= q <= n ==> Sum(a, p, q) <= Sum(a, k, m);
{
t, n := t + a[n], n + 1;
if (t < 0) {
c, t := n, 0;
} else if (s < t) {
k, m, s := c, n, t;
}
}
}
|
