Dafny: added some test programs

4 files changed, 101 insertions, 1 deletions

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 381b9cb1..9f7fad4e 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -34,3 +34,11 @@ Dafny program verifier finished with 5 verified, 0 errors
 -------------------- StoreAndRetrieve.dfy --------------------

 

 Dafny program verifier finished with 22 verified, 0 errors

+

+-------------------- MajorityVote.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

+

+-------------------- SegmentSum.dfy --------------------

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
new file mode 100644
index 00000000..0adba718
--- /dev/null
+++ b/Test/dafny2/MajorityVote.dfy
@@ -0,0 +1,63 @@
+method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)

+  requires 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

+  ensures k == K;  // find K

+{

+  k := a[0];

+  var n, c, s := 1, 1, 0;

+  while (n < |a|)

+    invariant 0 <= s <= n <= |a|;

+    invariant 2 * Count(a, s, |a|, K) > |a| - s;  // K has majority among a[s..]

+    invariant 2 * Count(a, s, n, k) > n - s;  // k has majority among a[s..n]

+    invariant c == Count(a, s, n, k);

+  {

+    if (a[n] == k) {

+      n, c := n + 1, c + 1;

+    } else if (2 * c > n + 1 - s) {

+      n := n + 1;

+    } else {

+      n := n + 1;

+      // We have 2*Count(a, s, n, k) == n-s, and thus the following lemma

+      // lets us conclude 2*Count(a, s, n, K) <= n-s.

+      Lemma_Unique(a, s, n, K, k);

+      // We also have 2*Count(a, s, |a|, K) > |a|-s, and the following lemma

+      // tells us Count(a, s, |a|, K) == Count(a, s, n, K) + Count(a, n, |a|, K),

+      // and thus we can conclude 2*Count(a, n, |a|, K) > |a|-n.

+      Lemma_Split(a, s, n, |a|, K);

+      k, n, c, s := a[n], n + 1, 1, n;

+    }

+  }

+  Lemma_Unique(a, s, |a|, K, k);  // both k and K have a majority, so K == k

+}

+

+ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)

+  requires 0 <= s <= t <= u <= |a|;

+  ensures Count(a, s, t, x) + Count(a, t, u, x) == Count(a, s, u, x);

+{

+  /* The postcondition of this method is proved automatically via Dafny's

+     induction tactic.  But if a manual proof had to be provided, it would

+     look like this:

+  if (s != t) {

+    Lemma_Split(a, s, t-1, u, x);

+  }

+  */

+}

+

+ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)

+  requires 0 <= s <= t <= |a|;

+  ensures x != y ==> Count(a, s, t, x) + Count(a, s, t, y) <= t - s;

+{

+  /* The postcondition of this method is proved automatically via Dafny's

+     induction tactic.  But if a manual proof had to be provided, it would

+     look like this:

+  if (s != t) {

+    Lemma_Unique(a, s, t-1, x, y);

+  }

+  */

+}

+

+function Count<T>(a: seq<T>, s: int, t: int, x: T): int

+  requires 0 <= s <= t <= |a|;

+{

+  if s == t then 0 else

+  Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0

+}

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;

+    }

+  }

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index a4796939..494a8721 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -15,7 +15,7 @@ for %%f in (
     COST-verif-comp-2011-3-TwoDuplicates.dfy

     COST-verif-comp-2011-4-FloydCycleDetect.dfy

     Intervals.dfy

-    StoreAndRetrieve.dfy

+    StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy

   ) do (

   echo.

   echo -------------------- %%f --------------------