Dafny: added COST Verification Competition challenge programs to test suite

1 files changed, 79 insertions, 0 deletions

diff --git a/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
new file mode 100644
index 00000000..f67d7870
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
@@ -0,0 +1,79 @@
+/*

+Rustan Leino, 5 Oct 2011

+

+COST Verification Competition, Challenge 1: Maximum in an array

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

+

+Given: A non-empty integer array a.

+

+Verify that the index returned by the method max() given below points to

+an element maximal in the array.

+

+public class Max {

+    public static int max(int[] a) {

+        int x = 0;

+        int y = a.length-1;

+

+        while (x != y) {

+            if (a[x] <= a[y]) x++;

+                else y--;

+        }

+        return x;

+    }

+}

+*/

+

+// Remarks:

+

+// The verification of the loop makes use of a local ghost variable 'm'.  To the

+// verifier, this variable is like any other, but the Dafny compiler ignores it.

+// In other words, ghost variables and ghost assignments (and specifications,

+// for that matter) are included in the program just for the purpose of reasoning

+// about the program, and they play no role at run time.

+

+// The only thing that needs to be human-trusted about this program is the

+// specification of 'max' (and, since verification challenge asked to prove

+// something about a particular piece of code, that the body of 'max', minus

+// the ghost constructs, is really that code).

+

+// 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 2 seconds)

+// without further human intervention.

+

+method max(a: array<int>) returns (x: int)

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

+  ensures 0 <= x < a.Length;

+  ensures forall i :: 0 <= i < a.Length ==> a[i] <= a[x];

+{

+  x := 0;

+  var y := a.Length - 1;

+  ghost var m := y;

+  while (x != y)

+    invariant 0 <= x <= y < a.Length;

+    invariant m == x || m == y;

+    invariant forall i :: 0 <= i < x ==> a[i] <= a[m];

+    invariant forall i :: y < i < a.Length ==> a[i] <= a[m];

+  {

+    if (a[x] <= a[y]) {

+      x := x + 1;  m := y;

+    } else {

+      y := y - 1;  m := x;

+    }

+  }

+  return x;

+}