home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / lclint.zip / lclint-2_3h-os2-bin.zip / test / db3 / eref.lcl < prev    next >
Text File  |  1997-09-03  |  800b  |  48 lines
  1. imports employee;
  2.  
  3. immutable type eref;
  4. constant eref eref_undefined;
  5.  
  6. spec immutable type map;
  7.  
  8. spec map m;
  9.  
  10. eref eref_alloc(void) map m; 
  11. {
  12.   modifies m;
  13.   /* ensures newInd(result, m^, m'); */
  14. }
  15.  
  16. bool eref_isDefined (eref er) map m; { }
  17.  
  18. void eref_free(eref er) map m; 
  19. {
  20.   /* requires er \in domain(m^); */
  21.   modifies m;
  22.   /* ensures m' = delete(m^, er); */
  23. }
  24.  
  25. void eref_assign(eref er, employee e) map m; 
  26. {
  27.   /* requires er \in domain(m^); */
  28.   modifies m;
  29.   /* ensures m' = assign(m^, er, e); */
  30. }
  31.  
  32. employee eref_get(eref er) map m; 
  33. {
  34.   /* requires er \in domain(m^); */
  35.   /* ensures result = m^[er]; */
  36. }
  37.  
  38. bool eref_equal(eref er1, eref er2) 
  39. {
  40.   /* ensures result = (er1 = er2); */
  41. }
  42.  
  43. void eref_initMod(void) map m; internalState;
  44. {
  45.   modifies m, internalState;
  46.   /* ensures m' = new; */
  47. }
  48.