Differences

This shows you the differences between two versions of the page.

@@ Line 1: / Line 1: @@
+====== Insertion and Removal from a Sorted List ======
+<code java>
+class SortedList
+    /* sorted list  */
+{
+    private static Node first;
+    /*:
+      private static specvar reach :: "obj => obj => bool";
+      vardefs
+        "reach == (% a b. rtrancl_pt (% x y. x..next=y) a b)";
+      public static specvar content :: objset;
+      vardefs
+        "content == {n. n ~= null & (first, n) : {(x,y). x..next = y}^*}";
+      invariant "tree [next]";
+      invariant "first = null | (ALL n. n..next ~= first)";
+      invariant "ALL x n. x ~= null & n ~= null & x..next = n --> n : content";
+      invariant "(ALL n. n : content & n..next ~= null --> n..key <= n..next..key)";
+   */
+   public static void add(Node nn)
+      /*: requires "nn ~= null & nn ~: content"
+        modifies content
+        ensures "content = old content Un {nn}"
+      */
+   {
+      if (first==null) {
+         first = nn;
+         nn.next = null;
+         return;
+      } else if (first.key >= nn.key) {
+         nn.next = first;
+         first = nn;
+         return;
+      }
+      Node prev = first;
+      Node current = first.next;
+      while ((current != null) && (current.key < nn.key)) {
+         prev = current;
+         current = current.next;
+      }
+      nn.next = current;
+      prev.next = nn;
+   }
+   public static void remove(Node nn)
+      /*: requires "nn ~= null"
+        modifies content
+        ensures "content = old content - {nn}"
+      */
+   {
+      Node prev = null;
+      Node current = first;
+      while ((current != null) && (current.key < nn.key)) {
+         prev = current;
+         current = current.next;
+      }
+      if (current == nn) {
+         if (prev != null) {
+            prev.next = current.next;
+         } else {
+            first = current.next;
+         }
+         current.next = null;
+      }
+   }
+}
+</code>