LARA

public /*: claimedby Hashtable */ class Node {
    public /*: claimedby Hashtable */ Object key;
    public /*: claimedby Hashtable */ Object value;
    public /*: claimedby Hashtable */ Node next;
}
 
class Hashtable {
    private Node[] table = null;
 
    /*:
     public ghost specvar content :: "(obj * obj) set" = "{}";
     public ghost specvar init :: "bool" = "False";
 
     static specvar h :: "(obj \<Rightarrow> int \<Rightarrow> int)";
     vardefs "h == (\<lambda> o1. (\<lambda> i1. ((abs (hashFunc o1)) mod i1)))";
 
     static specvar abs :: "(int \<Rightarrow> int)" 
     vardefs "abs == (\<lambda> i1. (if (i1 < 0) then (-i1) else i1))";
 
     static ghost specvar con :: "obj => (obj * obj) set" = "\<lambda> this. {}";
 
     invariant ContentDefInv:
     "init \<longrightarrow> content = {(k,v). (k,v) \<in> table.[(h k (table..length))]..con}";
 
     invariant TableNotNull: "init \<longrightarrow> table \<noteq> null";
     invariant TableHidden: "init \<longrightarrow> table \<in> hidden";
     invariant AllocInv: "table \<in> alloc";
 
     invariant NodeHidden1: 
     "init \<longrightarrow> (\<forall> i. 0 \<le> i \<and> i < table..length \<and> table.[i] \<noteq> null \<longrightarrow> table.[i] \<in> hidden)";
 
     invariant NodeHidden2:
     "\<forall> n. n \<in> Node \<and> n \<in> alloc \<and> n \<noteq> null \<and> n..next \<noteq> null \<longrightarrow> n..next \<in> hidden";
 
     invariant HashInv:
     "init \<longrightarrow> (\<forall> k. 0 \<le> (h k (table..length)) \<and> (h k (table..length)) < table..length)";
 
     invariant ElementAllocInv:
       "\<forall> i. 0 \<le> i \<and> i < table..length \<longrightarrow> table.[i] \<in> alloc";
 
     invariant FirstInjInv:
       "init \<longrightarrow> (\<forall> i x y. 
          y = x..next \<and> y \<noteq> null \<and> 0 \<le> i \<and> i < table..length \<longrightarrow> y \<noteq> table.[i])";
 
     invariant NextInjInv:
       "\<forall> x1 x2 y. y \<noteq> null \<and> y = x1..next \<and> y = x2..next \<longrightarrow> x1 = x2";
 
     invariant ElementInjInv:
       "init \<longrightarrow> (\<forall> ht i j. ht \<in> Hashtable \<and> ht \<in> alloc \<and> ht..init \<and> 0 \<le> i \<and> 
        i < ht..table..length \<and> 0 \<le> j \<and> j < table..length \<and> 
        ht..table.[i] = table.[j] \<and> table.[j] \<noteq> null \<longrightarrow> ht = this \<and> i = j)";
 
     invariant ElementTypeInv:
       "\<forall> i. 0 \<le> i \<and> i < table..length \<longrightarrow> table.[i] \<in> Node";
 
     public 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 Coherence: "init \<longrightarrow>
       (\<forall> i k v. 0 \<le> i \<and> i < table..length \<longrightarrow>
           (k,v) \<in> table.[i]..con \<longrightarrow> h k (table..length) = i)";
 
     invariant ConAlloc:
       "\<forall> z x y. z \<in> Node \<and> z \<in> alloc \<and> (x,y) \<in> z..con \<longrightarrow> x \<in> alloc \<and> y \<in> alloc";
 
     invariant ConNull: "\<forall> x. null..con = \<emptyset>";
 
     invariant ConDef:
       "ALL x. x : Node & x : Object.alloc & x ~= null -->
          x..con = 
	  {(x..Node.key, x..Node.value)} Un x..Node.next..con &
	  (ALL v. (x..Node.key, v) ~: x..Node.next..con)";
 
     invariant ConNonNull:
       "ALL z x y. z : Node & z : Object.alloc & z ~= null & 
       (x, y) : z..con --> x ~= null & y ~= null";
 
     invariant TableInjInv: 
       "\<forall> ht. ht..table = table \<and> table \<noteq> null \<longrightarrow> ht = this";
 
    */
 
    public Hashtable(int n)
    /*: requires "0 < n"
        modifies content, init
        ensures "init \<and> content = {}" */
    {
	int i = 0;
	table = new /*: hidden */ Node[n];
 
	//: "content" := "{}";
	//: "init" := "True";
 
	//: note NewNotHT: "table \<notin> Hashtable";
 
	{ //: localize;
	/*: note ElemInj1: 
            "\<forall> ht1 i j. ht1 \<in> Hashtable \<and> ht1 \<in> alloc \<and> ht1..init \<and> 
             0 \<le> i \<and> i < ht1..table..length \<and> 0 \<le> j \<and> j < table..length \<and> 
             ht1..table.[i] = table.[j] \<and> ht1..table.[i] \<noteq> null \<longrightarrow> ht1 = this \<and> i = j"; */
        /*: note ElemInj2: 
            "\<forall> ht2 i j. ht2 \<in> Hashtable \<and> ht2 \<in> alloc \<and> ht2..init \<and> 0 \<le> i \<and> 
             i < table..length \<and> 0 \<le> j \<and> j < ht2..table..length \<and> 
             table.[i] = ht2..table.[j] \<and> table.[i] \<noteq> null \<longrightarrow> this = ht2 \<and> i = j"; */
        /*: note ElemInjOther:
            "\<forall> ht1 ht2 i j. ht1 \<noteq> this \<and> ht2 \<noteq> this \<and> ht1 \<in> Hashtable \<and> ht1 \<in> alloc \<and> 
             ht1..init \<and> ht2 \<in> Hashtable \<and> ht2 \<in> alloc \<and> ht2..init \<and> 0 \<le> i \<and> 
             i < ht1..table..length \<and> 0 \<le> j \<and> j < ht2..table..length \<and> 
             ht1..table.[i] = ht2..table.[j] \<and> ht1..table.[i] \<noteq> null \<longrightarrow> ht1 = ht2 \<and> i = j"
            from ElementInjInv, NewNotHT; */
	/*: note ElemInjAll: "theinv ElementInjInv" 
	    from ElemInj1, ElemInj2, ElemInjOther; */
	}
 
	{ //: localize;
        /*: note CohThis: "\<forall> i k v. 0 \<le> i \<and> i < table..length \<and> (k,v) \<in> table.[i]..con \<longrightarrow> 
            h k (table..length) = i"; */
        /*: note CohOther: "\<forall> ht. ht \<noteq> this \<and> ht : alloc \<and> ht \<in> Hashtable \<and> ht..init \<longrightarrow>
            (\<forall> i k v. 0 \<le> i \<and> i < ht..table..length \<and> (k,v) \<in> ht..table.[i]..con \<longrightarrow> 
            h k (ht..table..length) = i)" from Coherence, NewNotHT; */
        /*: note CohAll: "theinv Coherence" from CohThis, CohOther; */
	}
 
	{ //: localize;
        //: note ElemTypeThis: "\<forall> i. 0 \<le> i \<and> i < table..length \<longrightarrow> table.[i] \<in> Node";
        /*: note ElemTypeOther: "\<forall> ht. ht \<noteq> this \<and> ht : alloc \<and> ht \<in> Hashtable \<longrightarrow> 
            (\<forall> i. 0 \<le> i \<and> i < ht..table..length \<longrightarrow> ht..table.[i] \<in> Node)"
            from ElementTypeInv, NewNotHT; */
        /*: note ElemTypeAll: "theinv ElementTypeInv" 
            from ElemTypeThis, ElemTypeOther; */
	}
 
	{ //: localize;
        /*: note FirstInjThis: "\<forall> i x y. y = x..next \<and> y \<noteq> null \<and> 0 \<le> i \<and> 
            i < table..length \<longrightarrow> y \<noteq> table.[i]"; */
        /*: note FirstInjOther: "\<forall> ht. ht : alloc \<and> ht : Hashtable \<and> ht \<noteq> this \<and> 
          ht..init \<longrightarrow> (\<forall> i x y. y = x..next \<and> y \<noteq> null \<and> 0 \<le> i \<and> i < ht..table..length \<longrightarrow> 
          y \<noteq> ht..table.[i])" from FirstInjInv, TableInjInv, NewNotHT; */
        /*: note FirstInjAll: "theinv FirstInjInv" 
            from FirstInjThis, FirstInjOther; */
	}
 
	{ //: localize;
        //: note TableEmpty: "\<forall> i. table.[i]..con = \<emptyset>";
        /*: note ContentThis: 
            "content = {(k,v). (k,v) \<in> table.[(h k (table..length))]..con}"
            from TableEmpty; */
	/*: note ContentOther: "\<forall> ht. ht : alloc \<and> ht : Hashtable \<and> ht \<noteq> this \<longrightarrow> 
	      ht..content = old (ht..content)"; */
        /*: note ContentPost: "theinv ContentDefInv" 
	    from ContentThis, ContentOther, ContentDef, NewNotHT; */
	}
 
	{ //: localize;
	/*: note NodeHiddenThis: 
	      "\<forall> i. 0 \<le> i \<and> i < table..length \<and> table.[i] \<noteq> null \<longrightarrow> table.[i] \<in> hidden"; */
	/*: note NodeHiddenOther:
	      "\<forall> ht. ht : alloc \<and> ht : Hashtable \<and> ht..init \<and> ht \<noteq> this \<longrightarrow> 
	      (\<forall> i. 0 \<le> i \<and> i < ht..table..length \<and> ht..table.[i] \<noteq> null \<longrightarrow> 
	      ht..table.[i] \<in> hidden)"
	    from NodeHidden1, TableInjInv, NewNotHT; */
	/*: note NodeHiddenAll: "theinv NodeHidden1" 
	    from NodeHiddenThis, NodeHiddenOther; */
	}
 
	{ //: localize;
	//: note ArrayLength: "0 < table..length";
	//: note HashFuncRel: "h = (\<lambda> o1. (\<lambda> i1. ((abs (hashFunc o1)) mod i1)))"; 
	/*: note HashThis: 
	    "\<forall> k. 0 \<le> (h k (table..length)) \<and> (h k (table..length)) < table..length"
	    from ArrayLength, HashFuncRel; */
	/*: note HashOther:
	    "\<forall> ht. ht \<noteq> this \<and> ht : alloc \<and> ht : Hashtable \<and> ht..init \<longrightarrow> 
	      (\<forall> k. 0 \<le> (h k (ht..table..length)) \<and> 
	      (h k (ht..table..length)) < ht..table..length)"
	    from HashInv, NewNotHT, TableInjInv; */
        //: note ShowHashInv: "theinv HashInv" from HashThis, HashOther;
	}
    }
 
    private int compute_hash(Object o1)
    /*: requires "o1 \<noteq> null \<and> init \<and> theinvs"
        ensures "result = h o1 (table..Array.length) \<and> 
	         0 \<le> result \<and> result < table..length \<and>
		 alloc = old alloc \<and> theinvs"
    */
    {
        int hc = o1.hashCode();
 
        if (hc < 0) { hc = -hc; }
 
        //: note LengthPos: "0 < table..length";
        //: note ResPos: "0 \<le> (hc mod table..length)" from Branch, LengthPos;
        /*: note ResLt: "(hc mod table..length) < table..length" 
            from Branch, LengthPos; */
 
        return (hc % table.length);
    }
 
    public boolean containsKey(Object k0)
    /*: requires "k0 \<noteq> null \<and> init"
        ensures "result = (EX v. ((k0, v) : content))"
     */
    {
        return containsKey0(k0);
    }
 
    private boolean containsKey0(Object k0)
    /*: requires "k0 \<noteq> null \<and> comment ''Init'' init \<and> theinvs"
        ensures "result = (EX v. ((k0, v) : content)) & theinvs"
    */
    {
	//: instantiate ContentThis: "theinv ContentDefInv" with "this";
	//: mp ContentRhs: "this \<in> alloc \<and> this \<in> Hashtable \<and> init \<longrightarrow> content = {(k,v). (k, v) \<in> table.[(h k (table..length))]..con}";
	int hc = compute_hash(k0);
	boolean res = bucketContainsKey(hc, k0);
        //: note HC: "hc = h k0 (table..length)";
        //: note InCon: "res = (\<exists> v. ((k0, v) \<in> table.[hc]..con))";
        /*: note ShowResult: "res = (\<exists> v. ((k0, v) \<in> content))" 
	  from InCon, HC, ContentRhs; */
	return res;
    }
 
    private boolean bucketContainsKey(int bucket_id, Object k0)
    /*: requires "init & theinvs & 0 <= bucket_id & 
                  bucket_id < table..Array.length"
	ensures "result = (EX v. ((k0, v) : table.[bucket_id]..con)) & 
	         theinvs"
     */
    {
        Node current = table[bucket_id];
        while /*: inv "current : Node & current : Object.alloc & theinvs &
		       (EX v. (k0, v) : table.[bucket_id]..con) = 
		       (EX v. (k0, v) : current..con)"
	       */
            (current != null) {
            if (current.key == k0) {
                return true;
            }
            current = current.next;
        }
        return false;
    }
 
    public Object remove1(Object k0)
    /*: requires "init & k0 ~= null & (EX v. (k0, v) : content)"
        modifies content
        ensures "content = old content \<setminus> {(k0, result)} &
	         (k0, result) : old content"
    */
    {
	return remove(k0);
    }
 
    private Object removeFirst(Object k0, int hc)
    /*: requires "comment ''Init'' init \<and> k0 \<noteq> null \<and> 
	          (\<exists> v. (k0, v) \<in> content) \<and>
	          comment ''KFound'' (k0 = table.[hc]..key) \<and> 
	          comment ''HCProps'' 
	          (0 \<le> hc \<and> hc < table..length \<and> hc = h k0 (table..length)) \<and> 
	          theinvs"
        modifies content, con, next, arrayState
        ensures "comment ''IndeedRemoved'' 
	         (content = old content \<setminus> {(k0, result)}) \<and>
                 comment ''IndeedWasThere'' ((k0, result) : old content) \<and>
	         comment ''frameArray'' 
	         (\<forall> a i. a \<noteq> table \<longrightarrow> a.[i] = old (a.[i])) \<and> 
	         theinvs" */
    {
	//: pickWitness v0::obj suchThat InContent: "(k0, v0) \<in> content";
 
	{ //: localize;
	//: instantiate ThisNodeHidden1: "theinv NodeHidden1" with "this";
	//: mp ThisNodeHidden1Rhs: "this \<in> alloc \<and> this \<in> Hashtable \<and> init \<longrightarrow> (\<forall> i. 0 \<le> i \<and> i < table..length \<and> table.[i] \<noteq> null \<longrightarrow> table.[i] \<in> hidden)";
        //: note HiddenLemma: "null \<in> hidden \<longrightarrow> table.[hc] \<in> hidden" from ThisNodeHidden1Rhs, HCProps;
	}
 
	Node f = table[hc];
        Node second = f.next;
        f.next = null;
        //: "f..con" := "{(f..Node.key, f..Node.value)}";
 
        table[hc] = second;
        //: "content" := "old content \<setminus> {(k0, v0)}";
 
        //: note ThisProps: "this \<in> alloc \<and> this \<in> Hashtable \<and> init";
	//: note FNonNull: "f \<noteq> null";
 
	{//: localize;
	 //: instantiate ThisContent: "old (theinv ContentDefInv)" with "this";
	 //: note OldContent: "old content = {(k,v). (k,v) \<in> old (table.[(h k (table..length))]..con)}" from ThisContent, ThisProps;
	}
 
	{//: localize;
	 //: instantiate ThisElementAlloc: "old (theinv ElementAllocInv)" with "this";
	 //: instantiate ThisElementType: "old (theinv ElementTypeInv)" with "this";
	 //: note FProps: "f \<in> Node \<and> f \<in> alloc" from ThisElementAlloc, ThisElementType, ThisProps, HCProps;
	}
 
	{//: localize;
	 //: instantiate FConDef: "old (theinv ConDef)" with "f";
	 //: noteThat VFound: "v0 = f..value" from InContent, OldContent, FConDef, KFound, FProps, FNonNull, HCProps;
	}
 
	{//: localize;
	 //: instantiate ThisFirstInj: "old (theinv FirstInjInv)" with "this";
	 //: noteThat Acyclic: "fieldRead (old next) (arrayRead (old arrayState) table hc) \<noteq> (arrayRead (old arrayState) table hc)" from FNonNull, FProps, HCProps, ThisFirstInj, ThisProps;
	}
 
	{
	    //: pickAny ht::obj;
	    {
		//: assuming h1: "ht : alloc & ht : Hashtable & ht..init";
		{
		    //: assuming NotThisHyp: "ht ~= this";
		    //: note n1: "fieldRead (old Hashtable.content) ht = {(k, v). (k, v) : (fieldRead (old Hashtable.con) (arrayRead (old Array.arrayState) (ht..table) (h k (ht..table..length))))}" from n1, h1, NotThisHyp, ContentDefInv;
		    //: note n2: "ht..table ~= table";
		    {
			//: pickAny k::obj, v::obj;
			{
			    //: assuming h2: "(k, v) : ht..content";
			    //: note n4: "arrayRead (old Array.arrayState) (ht..table) (h k (ht..table..length)) ~= arrayRead (old Array.arrayState) table hc" from ElementInjInv, h1, NotThisHyp, ThisProps, HCProps, HashInv, FNonNull;
			    //: note c4: "(k, v) : ht..table.[(h k (ht..table..length))]..con" from c4, h1, NotThisHyp, h2, n1, n2, n4;
			}
			//: note c3: "(k, v) : ht..content --> (k, v) : ht..table.[(h k (ht..table..length))]..con" forSuch k, v;
		    }
		    {
			//: pickAny k::obj, v::obj;
			{
			    //: assuming h3: "(k, v) : ht..table.[(h k (ht..table..length))]..con";
			    //: note n5: "arrayRead (old Array.arrayState) (ht..table) (h k (ht..table..length)) ~= arrayRead (old Array.arrayState) table hc" from n5, ElementInjInv, h1, NotThisHyp, ThisProps, HCProps, HashInv, FNonNull;
			    //: note c5: "(k, v) : ht..content" from c5, h1, NotThisHyp, h3, n1, n2, n5;
			}
			//: note c2: "(k, v) : ht..table.[(h k (ht..table..length))]..con --> (k, v) : ht..content" forSuch k, v;
		    }
		    //: note ContentOther: "ht..content = {(k, v). (k, v) : ht..table.[(h k (ht..table..length))]..con}" from c2, c3;
		}
		{
		    //: assuming ThisHyp: "ht = this";
		    {//: localize;
		     //: instantiate ThisElementInj: "old (theinv ElementInjInv)" with "this";
		     //: note ThisInj: "\<forall> i j. 0 \<le> i \<and> i < table..length \<and> 0 \<le> j \<and> j < table..length \<and> old (table.[i]) = old (table.[j]) \<and> old (table.[i]) \<noteq> null \<longrightarrow> i = j" from ThisElementInj, ThisProps;
		    }
		    //: note ContentThis: "ht..content = {(k,v). (k,v) \<in> ht..table.[(h k (ht..table..length))]..con}" from OldContent, ThisInj, ThisProps, KFound, VFound, Acyclic, ConDef, FProps, FNonNull, HashInv, HCProps, ThisHyp;
		}
		//: cases "ht = this", "ht ~= this" for "ht..content = {(k, v). (k, v) : ht..table.[(h k (ht..table..length))]..con}" from ContentThis, ContentOther;
		//: note ContentCases2: "ht..content = {(k, v). (k, v) : ht..table.[(h k (ht..table..length))]..con}" from ContentThis, ContentOther;
	    }
	    //: note ContentAll: "ht : alloc & ht : Hashtable & ht..init --> ht..content = {(k, v). (k, v) : ht..table.[(h k (ht..table..length))]..con}" forSuch ht;
	}
 
	//: noteThat NextNull: "(old next) null = null";
	/*: noteThat NewCoherence: "theinv Coherence"
	    from Coherence, Acyclic, ConDef, ConNull, NextNull, 
	      ElementAllocInv, ElementTypeInv, TableInjInv, FProps, HCProps; */
 
	/*: note AllHidden1: "theinv NodeHidden1"
	    from NodeHidden1, NodeHidden2, ThisProps,
	      FProps, FNonNull, TableInjInv, TableNotNull; */
 
        /*: note AllHidden2: "theinv NodeHidden2"
	    from NodeHidden2, NodeHidden1, ThisProps; */
 
	/*: noteThat FirstInjLemma: "theinv FirstInjInv" 
	    from FirstInjInv, NextInjInv; */
 
 	/*: noteThat ElemInj: "theinv ElementInjInv"
	    from ElementInjInv, FirstInjInv, TableInj, FProps, 
	      FNonNull, HCProps; */
 
        //: note SecondType: "second \<in> Node";
        /*: note ElemType: "theinv ElementTypeInv"
	    from ElementTypeInv, SecondType, NullNode; */
 
	{//: localize;
	 //: instantiate ThisFirstInj: "old (theinv FirstInjInv)" with "this";
	 //: note FNotRefByNext: "\<forall> x. x..next \<noteq> f" from ThisFirstInj, ThisProps, FNonNull, HCProps, FProps;
	}
 
	//: note NullProps: "null \<in> alloc \<and> null \<in> Node";
 
	/*: noteThat NewConDef: "theinv ConDef"
	    from ConDef, ConNull, ElementAllocInv, ElementTypeInv, 
	    FNotRefByNext, HCProps, NullProps, FProps; */
 
        return f.value;
    }
 
    private Object removefromBucket(Object k0, int hc)
    /*: requires "comment ''Init'' init \<and> k0 \<noteq> null \<and> 
	          (\<exists> v. (k0, v) \<in> content) \<and>
	          comment ''KNotFound'' (k0 \<noteq> table.[hc]..key) \<and> 
	          comment ''HCProps'' 
	          (0 \<le> hc \<and> hc < table..length \<and> hc = h k0 (table..length)) \<and> 
	          theinvs"
        modifies content, con, next, arrayState
        ensures "comment ''IndeedRemoved'' 
	         (content = old content \<setminus> {(k0, result)}) \<and>
                 comment ''IndeedWasThere'' ((k0, result) : old content) \<and>
	         comment ''frameArray'' 
	         (\<forall> a i. a \<noteq> table \<longrightarrow> a.[i] = old (a.[i])) \<and> 
	         theinvs" */
    {
	//: pickWitness v0::obj suchThat InContent: "(k0, v0) \<in> content";
 
        //: note ThisProps: "this \<in> alloc \<and> this \<in> Hashtable \<and> this \<noteq> null";
 
        Node f = table[hc];
        Node prev = f;
 
        //: "prev..con" := "prev..con \<setminus> {(k0, v0)}";
        //: "content"   := "old content \<setminus> {(k0, v0)}";
 
        /*: note InBucket: "(k0, v0) \<in> (fieldRead (old con) f)"
            from InContent, ContentDef, ThisProps, Init, HCProps; */
        /*: note FNonNull: "f \<noteq> null" 
            from PrevNotNull, InBucket, HCProps, ThisProps, ConDef, ConNull, 
	      Init, ElementAllocInv, ElementTypeInv; */
 
        Node current = prev.next;
 
	/*: note InNext: "(k0, v0) \<in> (fieldRead (old con) current)"
	    from InBucket, KNotFound, ConDef, ElementAllocInv,
	      ElementTypeInv, ThisProps, Init, FNonNull, HCProps; */
	/*: note CurrNotNull: "current \<noteq> null"
	    from InNext, ConNull; */
 
	/*: note PrevNode: "prev \<in> Node"
	    from ElementTypeInv, ThisProps, Init, HCProps; */
 
        /*: note PrevHidden: "prev \<in> hidden" 
            from NodeHidden1, HCProps, Init, ThisProps, FNonNull; */
 
        /*: note ConPreLoop: "\<forall> n. n \<in> Node \<and> n \<in> alloc \<and> n \<noteq> null \<and> 
	      n \<noteq> prev \<longrightarrow> n..con = {(n..key, n..value)} \<union> n..next..con \<and> 
	      (\<forall> v. (n..key, v) \<notin> n..next..con)"
	    from ConDef, FirstInjInv, Init, ThisProps, HCProps, FNonNull; */
 
	/*: note ConUncBef: 
	      "\<forall> ht i. ht \<noteq> this \<and> ht \<in> Hashtable \<and> ht \<in> alloc \<and> ht..init \<and> 
	       0 \<le> i \<and> i < ht..table..length \<longrightarrow> 
	       ht..table.[i]..con = old (ht..table.[i]..con)"
	    from ElementInjInv, ThisProps, Init, HCProps, FNonNull; */
 
	while /*: inv "prev \<in> Node \<and> prev \<in> alloc \<and> prev \<noteq> null \<and> 
	          prev \<in> hidden \<and>
	          comment ''PrevCon'' 
	          (prev..con = 
	          fieldRead (old con) prev \<setminus> {(k0, v0)}) \<and>
	          comment ''PrevNot'' 
	          (\<forall> v. (prev..key, v) \<notin> prev..next..con) \<and>
	          comment ''CurrProps'' (current \<in> Node \<and> current \<in> alloc) \<and> 
	          comment ''CurrNotNull'' (current \<noteq> null) \<and>
	          comment ''PrevCurr'' 
	          (prev..next = current \<and> prev \<noteq> current) \<and>
	          content = old content \<setminus> {(k0, v0)} \<and>
	          (k0, v0) \<in> current..con \<and>
	          comment ''ConDefInv''
		  (\<forall> n. n \<in> Node \<and> n \<in> alloc \<and> n \<noteq> null \<and> n \<noteq> prev \<longrightarrow>
	          n..con = {(n..key, n..value)} \<union> n..next..con \<and> 
	          (\<forall> v. (n..key, v) \<notin> n..next..con)) \<and>
	          comment ''ConLoop'' (ALL n. n..con = old (n..con) \<or> 
	          n..con = old (n..con) \<setminus> {(k0, v0)}) \<and> 
	          comment ''ConNull'' (null..con = \<emptyset>) \<and>
	          comment ''FConInv'' 
	          (f..con = (fieldRead (old con) f) \<setminus> {(k0, v0)}) \<and> 
	          comment ''ConUnchanged''
	          (\<forall> ht i. ht \<noteq> this \<and> ht \<in> Hashtable \<and> ht \<in> alloc \<and> 
	          ht..init \<and> 0 \<le> i \<and> i < ht..table..length \<longrightarrow> 
	          ht..table.[i]..con = old (ht..table.[i]..con))" */
	    (current.key != k0)
        {
            //: "current..con" := "current..con \<setminus> {(k0, v0)}";
 
	    /*: note CurrCon: "current..con = 
	        fieldRead (old con) current \<setminus> {(k0, v0)}"; */
	    //: note PrevIsNot: "prev..key \<noteq> k0";
	    /*: note OldConDef: "fieldRead (old con) prev = 
	        {(prev..key, prev..value)} \<union> 
	        fieldRead (old con) (prev..next)"; */
	    /*: note PrevConDef: 
	        "prev..con = {(prev..key, prev..value)} \<union> prev..next..con" 
	        from PrevCurr, PrevCon, CurrCon, OldConDef, PrevIsNot; */
 
            prev = current;
            current = current.next;
 
            /*: note FConLem: 
		  "f..con = (fieldRead (old con) f) \<setminus> {(k0, v0)}"
		from FConInv; */
 
            /*: note ConUncPre:
		  "\<forall> ht i. ht \<noteq> this \<and> ht \<in> Hashtable \<and> ht \<in> alloc \<and> 
	          ht..init \<and> 0 \<le> i \<and> i < ht..table..length \<longrightarrow> 
	          ht..table.[i]..con = old (ht..table.[i]..con)"
		from ConUnchanged, PrevCurr, FirstInjInv, CurrNotNull; */
 
            /*: note ConExceptPrev: "\<forall> n. n \<in> Node \<and> n \<in> alloc \<and> n \<noteq> null \<and> 
		  n \<noteq> prev \<longrightarrow> n..con = {(n..key, n..value)} \<union> n..next..con \<and> 
	          (\<forall> v. (n..key, v) \<notin> n..next..con)"
		from PrevConDef, PrevNot, ConDefInv, PrevCurr, NextInjInv, CurrNotNull; */
        }
 
	Node nxt = current.next;
	prev.next = nxt;
	current.next = null;
 
	//: "current..con" := "{(current..Node.key, current..Node.value)}";
 
	{
	    //: pickAny x::obj;
	    {
		//: assuming h1: "x : Node & x : Object.alloc & x ~= null";
		//: note n1: "x ~= prev --> fieldRead (old Node.next) x ~= current" from h1, NextInjInv, CurrNotNull, PrevCurr;
		//: note n2: "current..con = {(current..Node.key, current..Node.value)}";
		{
		    //: assuming h2: "x = current";
		    //: note c5: "x..con = {(x..Node.key, x..Node.value)} Un x..Node.next..con" from h1, h2, ConNull;
		}
		{
		    //: assuming h3: "x = prev";
		    //: note n3: "fieldRead (old Node.next) current ~= current" from NextInjInv, CurrNotNull, PrevCurr, CurrProps;			    
		    //: note n4: "prev..next..con = fieldRead (old Hashtable.con) (prev..next)";
		    //: note n5: "fieldRead (old Hashtable.con) prev = {(prev..key, prev..value)} Un fieldRead (old Hashtable.con) current";
		    //: note n6: "fieldRead (old Hashtable.con) current = {(current..key, current..value)} Un fieldRead (old Hashtable.con) (fieldRead (old Node.next) current)";
		    //: note n7: "prev..key ~= k0";
 
		    {
			//: pickAny k::obj, v::obj;
			{
			    //: assuming h4: "(k, v) : x..con";
			    //: note n8: "k ~= k0";
			    //: note n10: "current..key = k0";
			    //: note c8: "(k, v) : {(x..Node.key, x..Node.value)} Un x..Node.next..con" from h1, h3, h4, PrevCurr, n3, PrevCon, n4, n5, n6, n7, n8, n10;
			}
			//: note c6: "(k, v) : x..con --> (k, v) : {(x..Node.key, x..Node.value)} Un x..Node.next..con" forSuch k, v;
		    }
		    {
			//: pickAny k::obj, v::obj;
			{
			    //: assuming h5: "(k, v) : {(x..Node.key, x..Node.value)} Un x..Node.next..con";
			    //: note n9: "k ~= k0";
			    //: note c9: "(k, v) : x..con" from h1, h3, h5, PrevCurr, n3, n4, PrevCon, n5, n6, n7, n9;
			}
			//: note c7: "(k, v) : {(x..Node.key, x..Node.value)} Un x..Node.next..con --> (k, v) : x..con" forSuch k, v; 
		    }
		    //: note c4: "x..con = {(x..Node.key, x..Node.value)} Un x..Node.next..con" from c6, c7;
		}
		{
		    //: assuming h4: "x ~= current & x ~= prev";
		    //: note c3: "x..con = {(x..Node.key, x..Node.value)} Un x..Node.next..con" from h1, h4, n1, ConDef;
		}
		//: cases "x = current", "x = prev", "x ~= current & x ~= prev" for n4: "x..con = {(x..Node.key, x..Node.value)} Un x..Node.next..con";
		{
		    //: pickAny v::obj;
		    //: note c2: "(x..Node.key, v) ~: x..Node.next..con" forSuch v;
		}
		//: note c1: "x..con = {(x..Node.key, x..Node.value)} Un x..Node.next..con & (ALL v. (x..Node.key, v) ~: x..Node.next..con)";
	    }
	    //: note ConPost: "x : Node & x : Object.alloc & x ~= null --> x..con = {(x..Node.key, x..Node.value)} Un x..Node.next..con & (ALL v. (x..Node.key, v) ~: x..Node.next..con)" forSuch x;
	}
 
	{
	    //: pickAny ht::obj;
	    {
		//: assuming h1: "ht : alloc & ht : Hashtable & ht..init";
		{
		    //: pickAny i::int, k::obj, v::obj;
		    {
			//: assuming h2: "0 <= i & i < ht..table..length & (k, v) : ht..table.[i]..con";
			//: note n1: "ht..table.[i] ~= current";
			//: note c3: "h k (ht..table..length) = i" from h1, h2, Coherence, n1, ConLoop;
		    }
		    //: note c2: "0 <= i & i < ht..table..length --> (k, v) : ht..table.[i]..con --> h k (ht..table..length) = i" forSuch i, k, v;
		}
		//: note c1: "ALL i k v. 0 <= i & i < ht..table..length --> (k, v) : ht..table.[i]..con --> h k (ht..table..length) = i";
	    }
	    //: note CoherencePost: "ht : alloc & ht : Hashtable & ht..init --> (ALL i k v. 0 <= i & i < ht..table..length --> (k, v) : ht..table.[i]..con --> h k (ht..table..length) = i)" forSuch ht;
	}
 
	{
	    //: pickAny ht::obj;
	    {
		//: assuming h1: "ht : alloc & ht : Hashtable & ht..init";
		{
		    //: pickAny i::int, x::obj, y::obj;
		    {
			//: assuming h2: "y = x..next & y ~= null & 0 <= i & i < ht..table..length";
			//: note c4: "y ~= ht..table.[i]" from h1, h2, FirstInjInv, PrevCurr;
		    }
		    //: note c3: "y = x..next & y ~= null & 0 <= i & i < ht..table..length --> y ~= ht..table.[i]" forSuch i, x, y;
		}
		//: note c2: "ALL i x y. y = x..next & y ~= null & 0 <= i & i < ht..table..length --> y ~= ht..table.[i]";
	    }
	    //: note FirstInjPost: "ht : alloc & ht : Hashtable & ht..init --> (ALL i x y. y = x..next & y ~= null & 0 <= i & i < ht..table..length --> y ~= ht..table.[i])" forSuch ht;
	}
 
	{
	    //: pickAny x::obj;
	    {
		//: assuming h1: "x : alloc & x : Hashtable & x..init";
		//: note n1: "fieldRead (old Hashtable.content) x = {(k, v). (k, v) : fieldRead (old Hashtable.con) (arrayRead (old Array.arrayState) (x..table) (h k (x..table..length)))}" from h1, ContentDefInv;
		//: note n2: "ALL k. 0 <= (h k (x..table..length)) & (h k (x..table..length)) < (x..table..length)" from h1, HashInv;
		{
		    //: assuming h2: "x ~= this";
		    //: note n3: "ALL i. 0 <= i & i < x..table..length --> x..table.[i] ~= current";
		    //: note n4: "ALL i. 0 <= i & i < x..table..length --> x..table.[i]..con = fieldRead (old Hashtable.con) (arrayRead (old Array.arrayState) (x..table) i)" from h1, h2, n3, ConUnchanged;
		    //: note c3: "x..content = {(k, v). (k, v) : x..table.[(h k (x..table..length))]..con}" from h1, h2, n1, n2, n4;
		}
		{ 
		    //: assuming h3: "x = this";
		    //: note n5: "old content = {(k,v). (k,v) \<in> old (table.[(h k (table..length))]..con)}";
		    {
			//: pickAny k::obj, v::obj;
			{
			    //: assuming h4: "(k, v) : content";
			    //: note n6: "table.[(h k (table..length))] ~= current" from FirstInjInv, h1,h3, PrevCurr, CurrNotNull, HashInv;
			    //: note c5: "(k, v) : table.[(h k (table..length))]..con" from h4, n5, n6, ConLoop;
			}
			//: note c6: "(k, v) : content --> (k, v) : table.[(h k (table..length))]..con" forSuch k, v;
		    }
		    {
			//: pickAny k::obj, v::obj;
			{
			    //: assuming h5: "(k, v) : table.[(h k (table..length))]..con";
			    //: note n7: "table.[(h k (table..length))] ~= current" from FirstInjInv, h1, h3, PrevCurr, CurrNotNull, HashInv;
			    //: note c7: "(k, v) : content" from h5, n5, n7, ConLoop, FConInv, HCProps;
			}
			//: note c8: "(k, v) : table.[(h k (table..length))]..con --> (k, v) : content" forSuch k, v;
		    }
		    //: note c4: "content = {(k, v). (k, v) : table.[(h k (table..length))]..con}" from c6, c8;
		}
		//: note c2: "x..content = {(k, v). (k, v) : x..table.[(h k (x..table..length))]..con}" from c3, c4;
	    }
	    //: note ContentDefPost: "x : alloc & x : Hashtable & x..init --> x..content = {(k, v). (k, v) : x..table.[(h k (x..table..length))]..con}" forSuch x;
	}
        return current.value;
 
    }
 
    private Object remove(Object k0)
    /*: requires "theinvs \<and> (comment ''Init'' init) \<and> k0 \<noteq> null \<and> 
	         (\<exists> v. (k0, v) \<in> content)"
        modifies content, con, next, arrayState
        ensures "theinvs \<and> 
	         comment ''IndeedRemoved'' 
	         (content = old content \<setminus> {(k0, result)}) \<and> 
	         comment ''IndeedWasThere'' ((k0, result) : old content) \<and> 
		 comment ''frameArray'' 
	         (ALL a i. a ~= table --> a.[i] = old (a.[i]))"
    */
    {
	//: pickWitness v0::obj suchThat KeyInContent: "(k0, v0) \<in> content";
 
	int hc = compute_hash(k0);
	Node f = table[hc];
 
        /*: note ThisProps: 
            "this \<in> old alloc \<and> this \<in> alloc \<and> this \<in> Hashtable"; */
        /*: note HCProps: 
            "0 \<le> hc \<and> hc < table..Array.length \<and> hc = h k0 (table..length)"; */
	/*: noteThat KeyInBucket: "(k0, v0) : table.[hc]..con" 
            from HCProps, KeyInContent, ContentDef, Init, ThisProps; */
	/*: note FProps: "f \<in> Node \<and> f \<in> old alloc \<and> f \<in> alloc"
	    from ElementTypeInv, Init, ThisProps, ElementAllocInv, HCProps; */
	//: noteThat FNonNull: "f \<noteq> null" from FProps, KeyInBucket, ConNull;
 
	if (f.key == k0) {
 
	    return removeFirst(k0, hc);
 
	} else {
 
	    return removefromBucket(k0, hc);
	}
    }
 
    private void add(Object k0, Object v0)
    /*: requires "(comment ''Init'' init) \<and> k0 \<noteq> null \<and> v0 \<noteq> null \<and> 
                  \<not> (\<exists> v. (k0, v) \<in> content) \<and> theinvs"
        modifies content, arrayState, "new..con", "new..next", "new..value", "new..key"
        ensures "content = old content Un {(k0, v0)} \<and>
	        (\<forall> a i. a \<noteq> table \<longrightarrow> a.[i] = old (a.[i])) \<and> theinvs" */
    {
	int hc = compute_hash(k0);
	Node n = new /*: hidden */ Node();
	n.key = k0;
	n.value = v0;
	Node first = table[hc];
	n.next = first;
	//: "n..con" := "{(k0, v0)} Un first..con";
	table[hc] = n;
	//: "content" := "(old content) Un {(k0, v0)}";
 
        //: note NewNotHT: "n \<notin> Hashtable";
        //: note ThisProps: "this \<in> alloc \<and> this \<in> old alloc \<and> this \<in> Hashtable";
        //: note HCBounds: "0 \<le> hc \<and> hc < table..length";
	//: noteThat NewOldNEq: "n \<noteq> first";
 
        //: note ThisTableNotNull: "table \<noteq> null";
 
	/*: noteThat OldNotRefInTable: 
	  "\<forall> ht i. ht : alloc \<and> ht : Hashtable \<and> ht..init \<and> 0 \<le> i \<and> 
           i < ht..table..length \<and> first \<noteq> null \<longrightarrow> ht..table.[i] \<noteq> first"
	  from OldNotRefInTable, Init, ThisProps, HCBounds, ElementInjInvHash,
	    NewOldNEq, TableInjInvHash, NewNotHT, ThisTableNotNull; */
 
        //: note HashPost: "theinv HashInv" from HashPost, HashInv, NewNotHT;
 
	//: note KeyAlloc: "k0 \<in> alloc";
	//: note ValAlloc: "v0 \<in> alloc";
	/*: note FirstProps: "first \<in> Node \<and> first \<in> alloc \<and> first \<noteq> n"
	  from FirstProps, ThisProps, ElementTypeInv, HCBounds,
	    ElementAllocInv, NewNotHT; */
	/*: note ConAllocLemma: "theinv ConAlloc"
	    from ConAllocLemma, ConAlloc, KeyAlloc, ValAlloc, FirstProps; */
 
        /*: note NewHidden2: "n..next \<noteq> null \<longrightarrow> n..next \<in> hidden" 
            from NewHidden2, NodeHidden1, ThisProps, Init, HCBounds; */
	/*: note OldHidden2: 
	    "\<forall> m. m \<noteq> n \<and> m \<in> Node \<and> m \<in> alloc \<and> m \<noteq> null \<and> m..next \<noteq> null \<longrightarrow> 
	     m..next \<in> hidden"; */
	//: note AllHidden2: "theinv NodeHidden2" from AllHidden2, NewHidden2, OldHidden2;
 
        //: note NewHidden: "n \<in> hidden";
        /*: note ThisHidden1: 
            "\<forall> i. 0 \<le> i \<and> i < table..length \<and> table.[i] \<noteq> null \<longrightarrow> table.[i] \<in> hidden"
            from ThisHidden1, NodeHidden1, NewHidden, ThisProps, Init; */
	/*: note OtherHidden1:
	    "\<forall> ht. ht \<noteq> this \<and> ht \<in> alloc \<and> ht \<in> Hashtable \<and> ht..init \<longrightarrow> 
	     (\<forall> i. 0 \<le> i \<and> i < ht..table..length \<and> ht..table.[i] \<noteq> null \<longrightarrow> 
	      ht..table.[i] \<in> hidden)" from OtherHidden1, NodeHidden1, NewNotHT; */
	/*: note Hidden1All: "theinv NodeHidden1"
	    from Hidden1All, ThisHidden1, OtherHidden1; */
 
	//: noteThat AllocChange: "Object.alloc = old Object.alloc Un {n}";
	//: noteThat HProp: "hc = h k0 (table..Array.length)";
 
	/*: note NewNotRefThisArr: 
	    "\<forall> i. 0 \<le> i \<and> i < table..length \<longrightarrow> 
	      (arrayRead (old arrayState) table i) \<noteq> n";*/
	/*: noteThat NewNotRefArray:
	    "\<forall> a i. 0 \<le> i \<and> i < a..length \<longrightarrow> 
	      (arrayRead (old arrayState) a i) \<noteq> n"; */
 
	//: noteThat NewNotAlloc: "n \<notin> old alloc";
	/*: noteThat NewNotRefByNext: "\<forall> x. x..next \<noteq> n"
	  from NewOldNEq, NewNotAlloc, unalloc_lonely, NewNotRefByNext; */
 
	//: note NotInOldContent: "\<forall> v. (k0, v) \<notin> old content";
	/*: note NotInOldConFirst: 
	    "\<forall> v. (k0, v) \<notin> (fieldRead (old con) first)"
	    from NotInOldConFirst, NotInOldContent, ContentDef, ThisProps,
	      Init, HProp; */
	//: note FirstNotN: "first \<noteq> n";
	/*: noteThat NewConDef: "theinv ConDef" 
	  from NewConDef, ConDef, NewNotRefByNext, FirstNotN, 
	    NotInOldConFirst; */
 
	//: note NType: "n \<in> Node";
	/*: note ElemType: "theinv ElementTypeInv" 
	    from ElementTypeInv, NType, NewNotHT; */
 
	/*: note ElemInj: "theinv ElementInjInv" 
	    from ElemInj, ElementInjInv, ThisProps, NewNotHT, ElementAllocInv,
	      NewNotRefArray, TableInjInv, ThisTableNotNull; */
 
	{
	    //: pickAny ht::obj;
	    {
		//: assuming h1: "ht : alloc & ht : Hashtable & ht..init";
		{
		    //: pickAny i::int, k::obj, v::obj;
		    //: note g1: "arrayRead (old Array.arrayState) (ht..table) i ~= n";
		    //: note g2: "ht : old alloc";
		    {
			//: assuming h2: "0 <= i & i < ht..table..length & (k,v) : ht..table.[i]..con";
			{
			    //: assuming h3: "ht = this";
			    //: note c5: "h k (ht..table..length) = i" from c3, h1, h2, h3, Coherence, g1, g2, HProp;
			}
			{
			    //: assuming h4: "ht ~= this";
			    //: note g3: "ht..table ~= table";
			    //: note c4: "h k (ht..table..length) = i" from c4, h1, h2, h4, Coherence, g1, g2, g3;
			}
			//: note c3: "h k (ht..table..length) = i" from c4, c5;
		    }
		    //: note c2: "0 <= i & i < ht..table..length --> (k,v) : ht..table.[i]..con --> h k (ht..table..length) = i" forSuch i, k, v;
		}
		//: note c1: "ALL i k v. 0 <= i & i < ht..table..length --> (k,v) : ht..table.[i]..con --> h k (ht..table..length) = i";
	    }
	    //: note CohPost: "ht : alloc & ht : Hashtable & ht..init --> (ALL i k v. 0 <= i & i < ht..table..length --> (k,v) : ht..table.[i]..con --> h k (ht..table..length) = i)" forSuch ht;
	}
 
	{
	    //: pickAny ht::obj;
	    {
		//: assuming NewContentHyp: "ht \<in> alloc \<and> ht \<in> Hashtable \<and> ht..init";
		//: note ThisContent: "content = {(k,v). (k,v) \<in> table.[(h k (table..length))]..con}" from ThisContent, HProp, NewNotRefThisArr, HashInv, ContentDefInv,  ThisProps, Init;
		{
		    //: assuming OtherHyp: "ht ~= this";
		    //: note OtherContent: "ht..content = {(k,v). (k,v) \<in> ht..table.[(h k (ht..table..length))]..con}" from OtherHyp, NewContentHyp, ContentDefInvHash, NewNotHT, TableInjInvHash, NewNotRefArray, TableNotNullHash, HashInv;
		}
 
		//: cases "ht = this", "ht ~= this" for NewContentCases: "ht..content = {(k,v). (k,v) \<in> ht..table.[(h k (ht..table..length))]..con}" from ThisContent, OtherContent;
		//: note NewContentConc: "ht..content = {(k,v). (k,v) \<in> ht..table.[(h k (ht..table..length))]..con}";
	    }
	    //: note NewContentDef: "ht \<in> alloc \<and> ht \<in> Hashtable \<and> ht..init \<longrightarrow> ht..content = {(k,v). (k,v) \<in> ht..table.[(h k (ht..table..length))]..con}" forSuch ht;
	}
 
	/*: noteThat OldNotRefByNext: 
	  "\<forall> x. first \<noteq> null \<longrightarrow> old (x..next) \<noteq> first"
	  from FirstInjInv, Init, HCBounds, OldNotRefByNext, ThisProps; */
 
	/*: noteThat NewFirstInj: "theinv FirstInjInv"
	  from FirstInjInv, NewNotRefByNext, OldNotRefByNext, TableInjInv,
	    OldNotRefInTable, HCBounds, NewFirstInj, ThisProps, ElementInjInv,
	    NewNotHT; */
 
	/*: noteThat NewNextInj: "theinv NextInjInv"
	  from NextInjInv, OldNotRefByNext, NewNextInj; */
    }
 
    public void add1(Object k0, Object v0)
    /*: requires "init & k0 ~= null & v0 ~= null & 
                  ~(EX v. (k0, v) : content)"
        modifies content
        ensures "content = old content Un {(k0, v0)}"
    */
    {
        add(k0, v0);
    }
 
    public Object replace(Object k0, Object v0)
    /*: requires "init & k0 ~= null & v0 ~= null & (EX v. (k0, v) : content)"
        modifies content
	ensures "content = old content - {(k0, result)} Un {(k0, v0)} &
                 (k0, result) : old content"
    */
    {
	Object v1 = remove(k0);
	add(k0, v0);
	return v1;
    }
 
    public Object put(Object k0, Object v0)
    /*: requires "init & k0 ~= null & v0 ~= null"
        modifies content
	ensures "content = old content - {(k0, result)} Un {(k0, v0)} \<and>
	         (result = null \<longrightarrow> \<not> (\<exists> v. (k0, v) \<in> old content)) \<and>
		 (result \<noteq> null \<longrightarrow> (k0, result) \<in> old content)" */
    {
	if (containsKey0(k0)) {
            Object v1 = remove(k0);
            add(k0, v0);
	    return v1;
	} else {
	    add(k0, v0);
	    return null;
	}
    }
 
    public Object get(Object k0)
    /*: requires "(comment ''Init'' init) \<and> k0 \<noteq> null"
        ensures "(result \<noteq> null \<longrightarrow> (k0, result) \<in> content) \<and>
	         (result = null \<longrightarrow> \<not>(\<exists> v. (k0, v) \<in> content))"
 
    */
    {
	//: instantiate ContentInst: "theinv ContentDefInv" with "this";
	//: mp ContentIs: "this : alloc & this : Hashtable & init --> content = {(k, v). (k, v) \<in> table.[(h k (table..length))]..con}";
	int hc = compute_hash(k0);
	Node current = table[hc];
        //: note HCIs: "hc = h k0 (table..length)";
        /*: note InCurrent: "\<forall> v. (((k0, v) \<in> content) = ((k0, v) \<in> current..con))" 
	    from ContentIs, HCIs; */
 
        while /*: inv "\<forall> v. ((k0, v) \<in> content) = ((k0, v) \<in> current..con)" */
            (current != null) {
            if (current.key == k0) {
                return current.value;
            }
 
            current = current.next;
        }
        return null;
    }
 
    public boolean isEmpty()
    /*: requires "init"
        ensures "result = (content = {})";
    */
    {
	//: note ThisProps: "this \<in> alloc \<and> this : Hashtable \<and> init";
	int i = 0;
	while /*: inv "comment ''IBounds'' (0 \<le> i) \<and>
                       (\<forall> j. 0 \<le> j \<and> j < i \<longrightarrow> table.[j]..con = \<emptyset>)" */
	    (i < table.length) {
	    if (table[i] != null) {
		//: note ILT: "i < table..length";
		//: note INonEmpty: "table.[i]..con \<noteq> \<emptyset>";
		/*: note ContentNonEmpty: "content \<noteq> \<emptyset>" 
		    from INonEmpty, ContentDefInv, Coherence, 
		    IBounds, ILT, ThisProps; */
		return false;
	    }
	    i = i + 1;
	}
	//: note AllEmpty: "\<forall> j. 0 \<le> j \<and> j < table..length \<longrightarrow> table.[j]..con = \<emptyset>";
	/*: note ContentEmpty: "content = \<emptyset>" 
	    from AllEmpty, ContentDefInv, HashInv, ThisProps; */
	return true;
    }
 
}