LARA

public /*: claimedby SinglyLinkedList */ class Node {
    public Object data;
    public Node next;
    //: public ghost specvar con :: "objset" = "{}"
}
 
class SinglyLinkedList {
    private Node first;
 
    /*: 
     public specvar content :: "obj set";
     vardefs "content == first..con";
 
     public ensured invariant ContentAlloc:
     "\<forall> x. x \<in> content \<longrightarrow> x \<in> alloc";
 
     private static specvar edge :: "obj \<Rightarrow> obj \<Rightarrow> bool";
     vardefs "edge == (\<lambda> x y. (x \<in> Node \<and> y = x..next) \<or>
                              (x \<in> SinglyLinkedList \<and> y = x..first))";
 
     invariant InjInv:
     "\<forall> x1 x2 y. y \<noteq> null \<and> edge x1 y \<and> edge x2 y \<longrightarrow> x1=x2";
 
     invariant AllocInv: "first \<in> alloc";
 
     public ensured invariant NonNullInv: "\<forall> x. x \<in> content \<longrightarrow> x \<noteq> null";
 
     invariant ConAlloc:
     "\<forall> z x. z \<in> Node \<and> z \<in> alloc \<and> x \<in> z..con \<longrightarrow> x \<in> alloc";
 
     invariant ConNull:
     "\<forall> x. x \<in> Node \<and> x \<in> alloc \<and> x = null \<longrightarrow> x..con = {}";
 
     invariant ConDef:
     "\<forall> x. x \<in> Node \<and> x \<in> alloc \<and> x \<noteq> null \<longrightarrow>
           x..con = {x..data} \<union> x..next..con \<and> x..data \<notin> x..next..con";
 
     invariant ConNonNull:
     "\<forall> z x. z \<in> Node \<and> z \<in> alloc \<and> x \<in> z..con \<longrightarrow> x \<noteq> null"; */
 
    public SinglyLinkedList()
    /*: 
      modifies content 
      ensures "content = {}"
    */
    {
        first = null;
    }
 
    public void remove(Object d0)
    /*: requires "d0 \<noteq> null \<and> d0 \<in> content"
        modifies content
        ensures "content = old content - {d0} \<and> d0 \<in> old content"
    */
    {
	Node f = first;
	if (f.data == d0) {
	    Node second = f.next;
	    f.next = null;
	    //: "f..con" := "{f..data}";
	    first = second;
	} else {
	    Node prev = first;
	    /*: "prev..Node.con" := 
	        "prev..Node.con \<setminus> {d0}";
	    */
	    Node current = prev.next;
	    while /*: inv "
		    prev : Node & prev : Object.alloc & prev ~= null &
		    prev..Node.con = 
		     fieldRead (old Node.con) prev \<setminus> {d0} &
		    current : Node & current : Object.alloc & current ~= null &
		    prev..Node.next = current & prev ~= current &
		    content = old content \<setminus> {d0} &
		    (ALL n. n : SinglyLinkedList & n : old Object.alloc & 
		    n ~= this -->
		    n..content = old (n..content)) &
		    d0 : current..Node.con &
		    comment ''ConDefInv''
		    (ALL n. n : Node & n : Object.alloc & n ~= null & n ~= prev -->
		    n..Node.con = {n..Node.data} Un n..Node.next..Node.con &
		    (n..Node.data ~: n..Node.next..Node.con)) &
		    (ALL n. n..Node.con = old (n..Node.con) |
		    n..Node.con = old (n..Node.con) \<setminus> {d0}) &
		    null..Node.con = {}"
		  */
		(current.data != d0)
                {
                    /*: "current..Node.con" := 
		      "current..Node.con \<setminus> {d0}"; */
                    prev = current;
                    current = current.next;
                }
	    Node nxt = current.next;
	    prev.next = nxt;
	    current.next = null;
	    //: "current..Node.con" := "{current..Node.data}";
	}
    }
 
    public boolean contains(Object d0)
    /*: ensures "result = (d0 : content)"
     */
    {
        return contains0(d0);
    }
 
    private boolean contains0(Object d0)
    /*: requires "theinvs"
        ensures "result = (d0 : content) & theinvs"
    */
    {
        Node current = first;
        while /*: inv "current : Node & current : Object.alloc & 
                       ((d0 : content) = (d0 : current..Node.con))" */
            (current != null) {
            if (current.data == d0) {
                return true;
            }
            current = current.next;
        }
        return false;
    }
 
    public void add(Object d0)
    /*: requires "d0 ~= null & (d0 ~: content)"
        modifies content
        ensures "content = old content Un {d0}"
     */
    {
	Node n = new Node();
	n.data = d0;
	n.next = first;
	//: "n..Node.con" := "{d0} Un first..Node.con";
	first = n;
    }
 
    public boolean isEmpty()
    /*: ensures "result = (content = {})";
    */
    {
        return (first==null);
    }
 
}