This is an old revision of the document!
Insertion into Tree with Data and Size Fields
public final class Node { public /*: claimedby Tree */ Node right; public /*: claimedby Tree */ Node left; public /*: claimedby Tree */ Object data; } public class DataSizeTree { private static Node root; private static int size; /*: private static specvar inlist :: objset; public static specvar content :: objset; private vardefs "inlist == {x. rtrancl_pt (% x y. x..Node.left = y | x..Node.right = y) root x}"; private vardefs "content == {x. EX n. n ~= null & n : inlist & n..data = x}" invariant "tree [Node.left, Node.right]"; invariant "inlist <= Object.alloc"; 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 : inlist"; invariant "size = card content"; */ public static void add(Object e) /*: requires "e ~: content & e ~= null" modifies content ensures "content = old content Un {e}"; */ { Node n = root, p = null; boolean wentLeft = false; while (n != null) { //: havoc "wentLeft"; p = n; if (wentLeft) { n = n.left; } else { n = n.right; } } Node n = new Node(); n.data = e; if (p == null) { root = n; } else { if (wentLeft) { p.left = n; } else { p.right = n; } } size = size + 1; } }