1 files changed, 0 insertions, 79 deletions
diff --git a/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
deleted file mode 100644
index f67d7870..00000000
--- a/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
+++ /dev/null
@@ -1,79 +0,0 @@
-/*
-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;
-}