[svn] r6386: nemerle/trunk/tools/contracts/examples: . BagFixed.n BagFixed.ssc

[stn]

Log:
Renamed the namespace from Nemerle.Assertions to Nemerle.Contracts. Added an example in Spec# and it's Nemerle counterpart.

Author: stn
Date: Thu Jun  8 22:22:40 2006
New Revision: 6386

Added:
   nemerle/trunk/tools/contracts/examples/
   nemerle/trunk/tools/contracts/examples/BagFixed.n
   nemerle/trunk/tools/contracts/examples/BagFixed.ssc

Added: nemerle/trunk/tools/contracts/examples/BagFixed.n
==============================================================================
--- (empty file)
+++ nemerle/trunk/tools/contracts/examples/BagFixed.n	Thu Jun  8 22:22:40 2006
@@ -0,0 +1,69 @@
+using System;
+using Nemerle.Contracts;
+
+public class BagFixed
+invariant 0 <= count && count <= elems.get_Length()
+{
+  [NotNull] mutable elems : array[int];
+  [Microsoft.Contracts.SpecPublicAttribute]
+  mutable count : int; // Make this field [SpecPublic]!
+
+  public this([NotNull] initialElements : array[int]) {
+    this.count = initialElements.Length; // Guard this dereference!
+    mutable e = array (initialElements.Length); // Make initialElements a non-null parameter!
+    Array.Copy (initialElements, 0, e, 0, initialElements.Length); // Use the less restrictive Copy method!
+    this.elems = e;
+    base();
+  }
+
+  public this([NotNull] initialElements : array[int], start : int, howMany : int)
+    requires 0 <= start && 0 <= howMany
+    requires start + howMany <= initialElements.get_Length()
+  {
+    this.count = howMany;
+    mutable e = array (howMany);
+    Array.Copy(initialElements, start, e, 0, howMany); // Fix the fifth argument!
+    this.elems = e;
+    base();
+  }
+
+  public virtual RemoveMin() : int // make this virtual
+    requires 0 < this.count
+  {
+    expose (this){
+      mutable m = System.Int32.MaxValue;
+      mutable mindex = 0;
+
+      for (mutable i = 0; i < count; i++) // Add a loop invariant!
+        invariant 0 <= i && i <= count && 0 <= mindex && mindex < count
+      {
+        when (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!
+      m
+    }
+  }
+
+  public virtual Add (x : int) : void // make this virtual
+  {
+    expose (this){
+      when (count == elems.Length)
+      {
+        notnull mutable b = array(2*elems.Length + 1); // 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 Main () : void
+  {
+  }
+}
+

Added: nemerle/trunk/tools/contracts/examples/BagFixed.ssc
==============================================================================
--- (empty file)
+++ nemerle/trunk/tools/contracts/examples/BagFixed.ssc	Thu Jun  8 22:22:40 2006
@@ -0,0 +1,73 @@
+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 BagFixed
+{
+  int[]! elems;
+  [SpecPublic] int count; // Make this field [SpecPublic]!
+  invariant 0 <= count && count <= elems.Length;
+
+  public BagFixed(int[]! initialElements) {
+    this.count = initialElements.Length; // Guard this dereference!
+    int[] e = new int[initialElements.Length]; // Make initialElements a non-null parameter!
+    Array.Copy(initialElements, 0, e, 0, initialElements.Length); // Use the less restrictive Copy method!
+    this.elems = e;
+    base();
+  }
+
+  public BagFixed(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, howMany); // Fix the fifth argument!
+    this.elems = e;
+    base();
+  }
+
+  public virtual int RemoveMin() // make this virtual
+    requires 0 < this.count;
+  {
+    expose (this){
+      int m = System.Int32.MaxValue;
+      int mindex = 0;
+      for (int i = 0; i < count; i++) // Add a loop invariant!
+        invariant 0 <= i && i <= count && 0 <= mindex && mindex < count;
+      {
+        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 virtual void Add(int x) // make this virtual
+  {
+    expose (this){
+      if (count == elems.Length)
+      {
+        int[]! b = new int[2*elems.Length+1]; // 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 ()
+  {
+  }
+}