Fixed manual typo.

[splint.git] / test / db3 / 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; */
}