summaryrefslogtreecommitdiff
path: root/Test/dafny2/SegmentSum.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny2/SegmentSum.dfy')
-rw-r--r--Test/dafny2/SegmentSum.dfy29
1 files changed, 0 insertions, 29 deletions
diff --git a/Test/dafny2/SegmentSum.dfy b/Test/dafny2/SegmentSum.dfy
deleted file mode 100644
index dc67162b..00000000
--- a/Test/dafny2/SegmentSum.dfy
+++ /dev/null
@@ -1,29 +0,0 @@
-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;
- }
- }
-}