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 / db2 / eref.lcl < prev    next >
Text File  |  1997-09-03  |  721b  |  45 lines
  1. imports employee;
  2.  
  3. immutable type eref;
  4. spec immutable type map;
  5.  
  6. spec map m;
  7. constant eref erefNIL;
  8.  
  9. eref eref_alloc(void) map m; 
  10. {
  11.   modifies m;
  12.   /* ensures newInd(result, m^, m'); */
  13. }
  14.  
  15. void eref_free(eref er) map m; 
  16. {
  17.   /* requires er \in domain(m^); */
  18.   modifies m;
  19.   /* ensures m' = delete(m^, er); */
  20. }
  21.  
  22. void eref_assign(eref er, employee e) map m; 
  23. {
  24.   /* requires er \in domain(m^); */
  25.   modifies m;
  26.   /* ensures m' = assign(m^, er, e); */
  27. }
  28.  
  29. employee eref_get(eref er) map m; 
  30. {
  31.   /* requires er \in domain(m^); */
  32.   /* ensures result = m^[er]; */
  33. }
  34.  
  35. bool eref_equal(eref er1, eref er2) 
  36. {
  37.   /* ensures result = (er1 = er2); */
  38. }
  39.  
  40. void eref_initMod(void) map m; 
  41. {
  42.   modifies m;
  43.   /* ensures m' = new; */
  44. }
  45.