Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sortedlist.java [2009/01/30 12:24] (current)
wies created
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>​
 
sortedlist.java.txt · Last modified: 2009/01/30 12:24 by wies
 
© EPFL 2018 - Legal notice