Dafny: added some test programs

1 files changed, 29 insertions, 0 deletions

diff --git a/Test/dafny2/SegmentSum.dfy b/Test/dafny2/SegmentSum.dfy
new file mode 100644
index 00000000..dc67162b
--- /dev/null
+++ b/Test/dafny2/SegmentSum.dfy
@@ -0,0 +1,29 @@
+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;

+    }

+  }

+}