• English only

# Lab for Automated Reasoning and Analysis LARA

```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;
}
}
}```