Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

threadedtree.java [2009/01/30 12:21] (current)
wies created
Line 1: Line 1:
 +====== Insertion into a Sorted Threaded Tree ======
  
 +<code java>
 +public final class Node {
 +   ​public /*: claimedby Tree */ Node right;
 +   ​public /*: claimedby Tree */ Node left;
 +   ​public /*: claimedby Tree */ Node next;
 +   ​public /*: claimedby Tree */ int v;
 +}
 +
 +public class ThreadedTree
 +{
 +   ​private static Node root;
 +   ​private static Node first;
 +
 +   /*: public static specvar content :: objset;
 +       ​private vardefs "​content ==
 +        {x. rtrancl_pt (% x y. x..left = y | x..right = y) root x}";
 +
 +       ​invariant "tree [left, right]";​
 +
 +       ​invariant "root ~= null --> (ALL n. n..left ~= root & n..right ~= root)";​
 +       ​invariant "first ~= null --> (ALL n. n..next ~= first)";​
 +       ​invariant "​(first,​root) : {(x,y). x..next = y}^*";
 +
 +       ​invariant "ALL x y. x ~= null & y ~= null & (x..right = y | x..left = y) --> y : content";​
 +       ​invariant "ALL x y. x..next = y <->
 +          (x ~= null -->
 +            (x..right = null -->
 +               ((EX z. z..left = x) --> y..left = x) &
 +               ((ALL z. z..left ~= x) -->
 +                   ​(((ALL z. (left z, x) ~: {(x1,x2). x1..right = x2}^*)) & (y = null) |
 +                   (left y, x) : {(x1,x2). x1..right = x2}^*))) &
 +            (x..right ~= null -->
 +               ​y..left = null & y ~= null & (right x, y) : {(x1, x2). x1..left = x2}^*)) &
 +          (x = null --> y = null)";​
 +       ​invariant "ALL x. x : content & x ~= null & x..next ~= null --> x..v <= x..next..v";​
 +
 +   */
 +
 +   ​public static void add(Node e)
 +      /*:
 +        requires "e ~: content"​
 +        modifies content
 +        ensures "​content = old content Un {e}";
 +      */
 +   {
 +      Node n = root, p = null;
 +      Node pred = null;
 +      Node succ = null;
 +      boolean wentLeft = false;
 +      while (n != null) {
 +         p = n;
 +         if (e.v < n.v) {
 +            wentLeft = true;
 +            succ = n;
 +            n = n.left;
 +         } else {
 +            wentLeft = false;
 +            pred = n;
 +            n = n.right;
 +         }
 +      }
 +      if (p == null) {
 +         root = e;
 +      } else {
 +         if (wentLeft) {
 +            p.left = e;
 +         } else {
 +            p.right = e;
 +         }
 +      }
 +      e.next = succ;
 +      if (pred != null) pred.next = e;
 +   }
 +}
 +</​code>​
 
threadedtree.java.txt · Last modified: 2009/01/30 12:21 by wies