Dafny: added COST Verification Competition challenge programs to test suite

1 files changed, 118 insertions, 0 deletions

diff --git a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
new file mode 100644
index 00000000..069baa61
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
@@ -0,0 +1,118 @@
+/*

+Rustan Leino, 5 Oct 2011

+

+COST Verification Competition, Challenge 3: Two equal elements

+http://foveoos2011.cost-ic0701.org/verification-competition

+

+Given: An integer array a of length n+2 with n>=2. It is known that at

+least two values stored in the array appear twice (i.e., there are at

+least two duplets).

+

+Implement and verify a program finding such two values.

+

+You may assume that the array contains values between 0 and n-1.

+*/

+

+// Remarks:

+

+// The implementation of method 'Search' takes one pass through the elements of

+// the given array.  To keep track of what it has seen, it allocates an array as

+// temporary storage--I imagine that this is what the competition designers

+// had in mind, since the problem description says one can assume the values

+// of the given array to lie in the range 0..n.

+

+// To keep track of whether it already has found one duplicate, the method

+// sets the output variables p and q as follows:

+//   p != q   - no duplicates found yet

+//   p == q   - one duplicate found so far, namely the value stored in p and q

+// Note, the loop invariant does not need to say anything about the state

+// of two duplicates having been found, because when the second duplicate is

+// found, the method returns.

+

+// What needs to be human-trusted about this program is the specification of

+// 'Search'.  The specification straightforwardly lists the assumptions stated

+// in the problem description, including the given fact that the array contains

+// (at least) two distinct elements that each occurs (at least) twice.  To

+// trust the specification of 'Search', a human also needs to trust the definition

+// of 'IsDuplicate' and its auxiliary function 'IsPrefixDuplicate'.

+

+// About Dafny:

+// As always (when it is successful), Dafny verifies that the program does not

+// cause any run-time errors (like array index bounds errors), that the program

+// terminates, that expressions and functions are well defined, and that all

+// specifications are satisfied.  The language prevents type errors by being type

+// safe, prevents dangling pointers by not having an "address-of" or "deallocate"

+// operation (which is accommodated at run time by a garbage collector), and

+// prevents arithmetic overflow errors by using mathematical integers (which

+// is accommodated at run time by using BigNum's).  By proving that programs

+// terminate, Dafny proves that a program's time usage is finite, which implies

+// that the program's space usage is finite too.  However, executing the

+// program may fall short of your hopes if you don't have enough time or

+// space; that is, the program may run out of space or may fail to terminate in

+// your lifetime, because Dafny does not prove that the time or space needed by

+// the program matches your execution environment.  The only input fed to

+// the Dafny verifier/compiler is the program text below; Dafny then automatically

+// verifies and compiles the program (for this program in less than 11 seconds)

+// without further human intervention.

+

+function IsDuplicate(a: array<int>, p: int): bool

+  requires a != null;

+  reads a;

+{

+  IsPrefixDuplicate(a, a.Length, p)

+}

+

+function IsPrefixDuplicate(a: array<int>, k: int, p: int): bool

+  requires a != null && 0 <= k <= a.Length;

+  reads a;

+{

+  exists i,j :: 0 <= i < j < k && a[i] == a[j] == p

+}

+

+method Search(a: array<int>) returns (p: int, q: int)

+  requires a != null && 4 <= a.Length;

+  requires exists p,q :: p != q && IsDuplicate(a, p) && IsDuplicate(a, q);  // two distinct duplicates exist

+  requires forall i :: 0 <= i < a.Length ==> 0 <= a[i] < a.Length - 2;  // the elements of "a" in the range [0.. a.Length-2]

+  ensures p != q && IsDuplicate(a, p) && IsDuplicate(a, q);

+{

+  // allocate an array "d" and initialize its elements to -1.

+  var d := new int[a.Length-2];

+  var i := 0;

+  while (i < d.Length)

+    invariant 0 <= i <= d.Length && forall j :: 0 <= j < i ==> d[j] == -1;

+  {

+    d[i], i := -1, i+1;

+  }

+

+  i, p, q := 0, 0, 1;

+  while (true)

+    invariant 0 <= i < a.Length;

+    invariant forall j :: 0 <= j < d.Length ==>

+                (d[j] == -1 && forall k :: 0 <= k < i ==> a[k] != j) ||

+                (0 <= d[j] < i && a[d[j]] == j);

+    invariant p == q ==> IsDuplicate(a, p);

+    invariant forall k :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];

+    decreases a.Length - i;

+  {

+    var k := d[a[i]];

+    assert k < i;  // note, this assertion is really for human consumption; it is not needed by the verifier, and it does not change the performance of the verifier

+    if (k == -1) {

+      // a[i] does not exist in a[..i]

+      d[a[i]] := i;

+    } else {

+      // we have encountered a duplicate

+      assert a[i] == a[k] && IsDuplicate(a, a[i]);  // note, this assertion is really for human consumption; it is not needed by the verifier, and it does not change the performance of the verifier

+      if (p != q) {

+        // this is the first duplicate encountered

+        p, q := a[i], a[i];

+      } else if (p == a[i]) {

+        // this is another copy of the same duplicate we have seen before

+      } else {

+        // this is the second duplicate

+        q := a[i];

+        return;

+      }

+    }

+    i := i + 1;

+  }

+}