Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

treeinsertion.java [2010/05/25 10:48] (current)
vkuncak created
Line 1: Line 1:
 +<code java>
 +public class Tree
 +{
 +   ​private static Node root;
 +   
 +   /*: public static specvar content :: objset;
 +       ​private vardefs "​content == 
 +        {x. rtrancl_pt (% x y. x..Node.left = y | x..Node.right = y) root x}";
 +   
 +       ​invariant "tree [Node.left, Node.right]";​
 +   
 +       ​invariant "root = null | (ALL n. n..Node.left ~= root & n..Node.right ~= root)";​
 +   
 +       ​invariant "ALL x y. x ~= null & y ~= null & (x..Node.right = y | x..Node.left = y) --> y : content";​
 +
 +       ​invariant "ALL x y. Node.parent x = y -->
 +                     (x ~= null & (EX z. z..Node.left = x | z..Node.right = x) --> (y..Node.left = x | y..Node.right = x))
 +           & (x = null | (ALL z. z..Node.left ~= x & z..Node.right ~= x) --> y = null)";​
 +
 +   */
 +    ​
 +   ​public static void add(Node e, int v) 
 +      /*: 
 + requires "e ~: content"​
 + modifies content
 + ensures "​content = old content Un {e}";
 +      */
 +   {
 +      Node n = root, p = null;
 +      boolean wentLeft = false;
 +      while (n != null) {
 + p = n;
 + if (v < n.v) {
 +     wentLeft = true;
 +            n = n.left;
 + } else {
 +     wentLeft = false;
 +     n = n.right;
 + }
 +      }
 +      e.v = v;
 +      if (p == null) {
 + root = e;
 +      } else {
 + e.parent = p;
 + if (wentLeft) {
 +            p.left = e;
 + } else {
 +            p.right = e;
 + }
 +      }
 +   }
 +</​code>​
  
 
treeinsertion.java.txt · Last modified: 2010/05/25 10:48 by vkuncak
 
© EPFL 2018 - Legal notice