[svn] r6388: nemerle/trunk/tools/contracts: examples/BagBroken.ssc main.n

[stn]

Log:
Added the license info to contracts, plus added original example, which is then annotated with contracts.

Author: stn
Date: Fri Jun  9 17:53:16 2006
New Revision: 6388

Added:
   nemerle/trunk/tools/contracts/examples/BagBroken.ssc
Modified:
   nemerle/trunk/tools/contracts/main.n

Added: nemerle/trunk/tools/contracts/examples/BagBroken.ssc
==============================================================================
--- (empty file)
+++ nemerle/trunk/tools/contracts/examples/BagBroken.ssc	Fri Jun  9 17:53:16 2006
@@ -0,0 +1,68 @@
+using System;
+using Microsoft.Contracts;
+
+/*\
+ * Note: The Spec# Program Verifier requires the file simplify.exe.
+ * The file simplify.exe is not shipped with Spec#. See the Spec#
+ * web site (http://research.microsoft.com/specsharp/) for
+ * instructions on how to obtain and install simplify.exe.
+\*/
+
+public class Bag
+{
+  int[]! elems;
+  int count; // Make this field [SpecPublic]!
+  invariant 0 <= count && count <= elems.Length;
+
+  public Bag(int[] initialElements) {
+    this.count = initialElements.Length; // Guard this dereference!
+    int[] e = new int[initialElements.Length]; // Make initialElements a non-null parameter!
+    initialElements.CopyTo(e, 0); // Use the less restrictive Copy method!
+    this.elems = e;
+    base();
+  }
+
+  public Bag(int[]! initialElements, int start, int howMany)
+    requires 0 <= start && 0 <= howMany;
+    requires start + howMany <= initialElements.Length;
+  {
+    this.count = howMany;
+    int[] e = new int[howMany];
+    Array.Copy(initialElements, start, e, 0, start+howMany); // Fix the fifth argument!
+    this.elems = e;
+    base();
+  }
+
+  public int RemoveMin() // make this virtual
+  {
+      int m = System.Int32.MaxValue;
+      int mindex = 0;
+      for (int i = 0; i < count; i++) // Add a loop invariant!
+      {
+        if (elems[i] < m) {
+          mindex = i;
+          m = elems[i];
+        }
+      }
+      count--; // Make sure the object is exposed when you assign to its fields, potentially causing the object invariant not to hold!
+      elems[mindex] = elems[count]; // Add a precondition requiring at least one element in the bag!
+      return m;
+  }
+
+  public void Add(int x) // make this virtual
+  {
+      if (count == elems.Length)
+      {
+        int[]! b = new int[2*elems.Length]; // Always grow the array, even if elems.Length == 0!
+        Array.Copy(elems, 0, b, 0, elems.Length);
+        elems = b;
+      }
+      elems[this.count] = x;
+      count++; // Make sure the object is exposed when you assign to its fields, potentially causing the object invariant not to hold!
+  }
+
+  public static void Main ()
+  {
+  }
+}
+

Modified: nemerle/trunk/tools/contracts/main.n
==============================================================================
--- nemerle/trunk/tools/contracts/main.n	(original)
+++ nemerle/trunk/tools/contracts/main.n	Fri Jun  9 17:53:16 2006
@@ -1,3 +1,31 @@
+/*
+ * Copyright (c) 2005 The University of Wroclaw.
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ *    1. Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *    2. Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *    3. The name of the University may not be used to endorse or promote
+ *       products derived from this software without specific prior
+ *       written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE UNIVERSITY ``AS IS'' AND ANY EXPRESS OR
+ * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
+ * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN
+ * NO EVENT SHALL THE UNIVERSITY BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
+ * TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
 using Nemerle.IO;
 using Nemerle.Utility;
 using Nemerle.Collections;
@@ -13,7 +41,7 @@
 using MC = Microsoft.Contracts;
 using SC = System.Compiler;
 
-namespace Nemerle.Assertions
+namespace Nemerle.Contracts
 {
   /*-------------------------- Invariant --------------------------*/