eref.lcl

imports employee;
 
immutable type eref;
constant eref eref_undefined;
 
spec immutable type map;
 
spec map m;
 
eref eref_alloc(void) map m; 
{
  modifies m;
  /* ensures newInd(result, m^, m'); */
}
 
bool eref_isDefined (eref er) map m; { }
 
void eref_free(eref er) map m; 
{
  /* requires er \in domain(m^); */
  modifies m;
  /* ensures m' = delete(m^, er); */
}
 
void eref_assign(eref er, employee e) map m; 
{
  /* requires er \in domain(m^); */
  modifies m;
  /* ensures m' = assign(m^, er, e); */
}
 
employee eref_get(eref er) map m; 
{
  /* requires er \in domain(m^); */
  /* ensures result = m^[er]; */
}
 
bool eref_equal(eref er1, eref er2) 
{
  /* ensures result = (er1 = er2); */
}
 
void eref_initMod(void) map m; internalState;
{
  modifies m, internalState;
  /* ensures m' = new; */
}