LARA

/* Imperative instantiable association list. */
 
public /*: claimedby AssociationList */ class Node {
    public Object key;
    public Object value;
    public Node next;
    //: public ghost specvar cnt :: "(obj * obj) set" = "{}"
}
 
class AssociationList {
    private Node first;  
    /*:
    public specvar content :: "(obj * obj) set";
    vardefs "content == first..cnt";
 
    private static specvar edge :: "obj \<Rightarrow> obj \<Rightarrow> bool";
    vardefs "edge == (\<lambda> x y. (x \<in> Node \<and> y = x..next) \<or>  
                             (x \<in> AssociationList \<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 CntNull:
    "\<forall> x. x \<in> Node \<and> x \<in> alloc \<and> x = null \<longrightarrow> x..cnt = {}";
 
    invariant CntDef:
    "\<forall> x. x \<in> Node \<and> x \<in> alloc \<and> x \<noteq> null \<longrightarrow>
	  x..cnt = {(x..key, x..value)} \<union> x..next..cnt \<and>
          (\<forall> v. (x..key, v) \<notin> x..next..cnt)";
 
    public ensured invariant SetInv:
    "\<forall> k v0 v1. (k, v0) \<in> content \<and> (k, v1) \<in> content \<longrightarrow> v0 = v1";
    public ensured invariant NonNullInv:
    "\<forall> k v. (k, v) \<in> content \<longrightarrow> k \<noteq> null \<and> v \<noteq> null";
    invariant CntAlloc:
    "\<forall> z x y. z \<in> Node \<and> z \<in> alloc \<and> (x, y) \<in> z..cnt \<longrightarrow> x \<in> alloc \<and> y \<in> alloc";
    invariant CntNonNull:
    "\<forall> z x y. z \<in> Node \<and> z \<in> alloc \<and> (x, y) \<in> z..cnt \<longrightarrow> x \<noteq> null \<and> y \<noteq> null";
    */
 
    public AssociationList()
    /*: modifies "this..content"
        ensures "content = {}" */
    {
	first = null;
    }
 
    public boolean containsKey(Object k0)
    //: ensures "result = (\<exists> v. ((k0, v) \<in> content))"
    {
        return containsKey0(k0);
    }
 
    private boolean containsKey0(Object k0)
    /*: requires "theinvs"
        ensures "result = (\<exists> v. ((k0, v) \<in> content)) \<and> theinvs" */
    {
        Node current = first;
        while //: inv "(\<exists> v. (k0, v) \<in> content) = (\<exists> v. (k0, v) \<in> current..cnt)"
            (current != null) {
            if (current.key == k0) {
                return true;
            }
            current = current.next;
        }
        return false;
    }
 
    public void add(Object k0, Object v0)
    /*: requires "k0 \<noteq> null \<and> v0 \<noteq> null \<and> \<not>(\<exists> v. (k0, v) \<in> content)"
        modifies content
        ensures "content = old content \<union> {(k0, v0)}" */
    {
	add0(k0, v0);
    }
 
    private void add0(Object k0, Object v0)
    /*: requires "theinvs \<and> k0 \<noteq> null \<and> v0 \<noteq> null \<and> \<not>(\<exists> v. (k0, v) \<in> content)"
        modifies content, "new..key", "new..value", "new..next", "new..cnt", first
        ensures "theinvs \<and> content = old content \<union> {(k0, v0)}" */
    {
	Node n = new Node();
	n.key = k0;
	n.value = v0;
	n.next = first;
	//: "n..cnt" := "{(k0, v0)} \<union> first..cnt";
	first = n;
    }
 
    public Object replace(Object k0, Object v0)
    /*: requires "k0 \<noteq> null \<and> v0 \<noteq> null \<and> (\<exists> v. (k0, v) \<in> content)"
        modifies content
	ensures "content = old content - {(k0, result)} \<union> {(k0, v0)} \<and>
                 (k0, result) \<in> old content" */
    {
        Object v1 = remove0(k0);
        add0(k0, v0);
        return v1;
    }
 
    public Object put(Object k0, Object v0)
    /*: requires "k0 \<noteq> null \<and> v0 \<noteq> null"
        modifies content
	ensures "content = old content - {(k0, result)} \<union> {(k0, v0)} \<and>
                 ((result \<noteq> null) = ((k0, result) \<in> old content)) \<and>
                 ((result = null) = (\<not>(\<exists> v. (k0, v) \<in> old content)))" */
    {
	if (containsKey0(k0)) {
	    Object v1 = remove0(k0);
	    add0(k0, v0);
	    return v1;
	} else {
	    add0(k0, v0);
	    return null;
	}
    }
 
    public Object get(Object k0)
    /*: requires "k0 \<noteq> null"
        ensures "((result \<noteq> null) = ((k0, result) \<in> content)) \<and>
	         ((result = null) = (\<not>(\<exists> v. (k0, v) \<in> content)))" */
    {
	Node current = first;
        while //: inv "\<forall> v. ((k0, v) \<in> content) = ((k0, v) \<in> current..cnt)"
            (current != null) {
            if (current.key == k0) {
                return current.value;
            }
            current = current.next;
        }
        return null;
    }
 
    public boolean isEmpty()
    /*: ensures "result = (content = {})"; */
    {
        return (first==null);
    }
 
    public Object remove(Object k0)
    /*: requires "k0 \<noteq> null \<and> (\<exists> v. (k0, v) \<in> content)"
        modifies content
        ensures "content = old content - {(k0, result)} \<and>
	         (k0, result) \<in> old content" */
    {
	return remove0(k0);
    }
 
    private Object remove0(Object k0)
    /*: requires "theinvs \<and> k0 \<noteq> null \<and> (\<exists> v. (k0, v) \<in> content)"
        modifies content, first, "Node.next", "Node.cnt"
        ensures "theinvs \<and>
	         content = old content - {(k0, result)} \<and>
	         (k0, result) \<in> old content" */
    {
	//: pickWitness v0 :: obj suchThat "(k0, v0) \<in> content";
	Node f = first;
	if (f.key == k0) {
	    Node second = f.next;
	    f.next = null;
	    //: "f..cnt" := "{(f..key, f..value)}";
	    first = second;
	    return f.value;
	} else {
	    Node prev = first;
	    //: "prev..cnt" := "prev..cnt - {(k0, v0)}";
	    Node current = prev.next;
	    while /*: inv "prev \<noteq> null \<and>
		    prev..cnt = prev..(old cnt) - {(k0, v0)} \<and> current \<noteq> null \<and>
		    prev..next = current \<and> prev \<noteq> current \<and>
		    content = old content - {(k0, v0)} \<and>
		    (\<forall> n. n \<in> AssociationList \<and> n \<in> old alloc \<and> n \<noteq> this \<longrightarrow>
		    n..content = old (n..content)) \<and>
		    (k0, v0) \<in> current..cnt \<and>
		    comment ''CntDefInv''
		    (\<forall> n. n \<in> Node \<and> n \<in> alloc \<and> n \<noteq> null \<and> n \<noteq> prev \<longrightarrow>
		    n..cnt = {(n..key, n..value)} \<union> n..next..cnt \<and>
		    (\<forall> v. (n..key, v) \<notin> n..next..cnt)) \<and>
		    (\<forall> n. n..cnt = old (n..cnt) \<or> 
                          n..cnt = old (n..cnt) - {(k0, v0)}) \<and>
		    null..cnt = {}"
		  */
		(current.key != k0)
                {
                    //: "current..cnt" := "current..cnt - {(k0, v0)}"; 
                    prev = current;
                    current = current.next;
                }
	    Node nxt = current.next;
	    prev.next = nxt;
	    current.next = null;
	    //: "current..cnt" := "{(current..key, current..value)}";
	    return current.value;
	}
    }
}