imports eref;

mutable type erc;
mutable type ercIter;

erc erc_create(void) 
{
  /* ensures fresh(result) /\ result' = { }; */
}

void erc_clear(erc c) 
{
  /* requires c^.activeIters = 0; */
  modifies c;
  /* ensures c' = { }; */
}

void erc_insert(erc c, eref er) 
{
  /* requires c^.activeIters = 0 /\ er \neq erefNIL; */
  modifies c;
  /* ensures c' = [insert(er, c^.val), 0]; */
}

bool erc_delete(erc c, eref er) 
{
  /* requires c^.activeIters = 0; */
  modifies c;
  /* ensures result = er \in c^.val
     /\ c' = [delete(er, c^.val), 0]; */
}

bool erc_member(eref er, erc c) 
{
  /* ensures result = er \in c^.val; */
}

eref erc_choose(erc c) 
{
  /* requires size(c^.val) \neq 0; */
  /* ensures result \in c^.val; */
}

int erc_size(erc c) 
{
  /* ensures result = size(c^.val); */
}

ercIter erc_iterStart(erc c) 
{
  modifies c;
  /* ensures fresh(result) /\ result' = [c^.val, c]
        /\ c' = startIter(c^);
  */
}

eref erc_yield(ercIter it) 
{
  modifies it; /* , it^.eObj */ 
  /* ensures if it^.toYield \neq { }
     then yielded(result, it^, it')
       /\ (it^.eObj)' = (it^.eObj)^
     else result = erefNIL /\ trashed(it)
       /\ (it^.eObj)' = endIter((it^.eObj)^);
 */
}

void erc_iterFinal(ercIter it) 
{
  modifies it; /* , it^.eObj; */
  /* ensures trashed(it)
     /\ (it^.eObj)' = endIter((it^.eObj)^);
  */
}

void erc_join(erc c1, erc c2) 
{
  /* requires c1^.activeIters = 0; */
  modifies c1;
  /* ensures c1' = [c1^.val \U c2^.val, 0]; */
}

char *erc_sprint(erc c) 
{
  /* ensures isSprint(result[]', c^) /\ fresh(result[]); */
}

void erc_final(erc c) 
{
  modifies c;
  /* ensures trashed(c); */
}

void erc_initMod(void) 
{
  ensures true;
}