# LARA

Main points: * new and improved: we define 'reachable' predicate * write code for removeMaybe spec, including loop invariant * write code for remove, including loop invariant

```class Node { public /*: claimedby SLL */ Node next; }
class SLL
{
private static Node root;
/*:
private static specvar reachable :: "obj => obj => bool";
private vardefs "reachable == (% x y.
(x,y) : {(u,v). u..next = v}^*)";

public static specvar content :: objset;
private vardefs "content ==  {x. x ~= null & reachable root x}";

invariant tree: "tree [next]";

invariant rootFirst: "root = null |
(ALL n. n..next ~= root)";
*/
/*:
requires "n ~: content & n ~= null & n..next = null &
(ALL m. m..next ~= n)"
modifies content
ensures "content = old content Un {n}";
*/
{
if (root == null) {
root = n;
n.next = null;
return;
}

Node r = root;
while //: inv "r : content"
(r.next != null) {
r = r.next;
}
r.next = n;
}

public static void remove(Node n)
/*: requires "n : content"
modifies content
ensures "content = old content - {n}"
*/
{
if (root == n) {
root = root.next;
n.next = null;
} else {
Node r = root;
//: assert "reachable r n"
while //: inv "r ~= n & r : content & reachable r n"
(r.next != n) {
r = r.next;
}
r.next = n.next;
n.next = null;
}
}

public static void removeMaybe(Node n)
/*: requires "(n : content)"
modifies content
ensures "content = old content
| content = old content - {n}"
*/
{
//: assert "n ~= null";
if (root == n) {
root = root.next;
n.next = null;
} else {
Node r = root;
while //: inv "r : content | r = null"
(r != null && r.next != n) {
r = r.next;
}
if (r != null) {
//: assert "r..next = n"
r.next = n.next;
n.next = null;
}
}
}
}```