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;
+}