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 / ereftab.lcl < prev    next >
Text File  |  1997-09-03  |  604b  |  37 lines
  1. imports employee, eref;
  2.  
  3. mutable type ereftab; 
  4.  
  5. ereftab ereftab_create(void) 
  6. {
  7.   /* ensures result' = empty; */
  8. }
  9.  
  10. void ereftab_insert(ereftab t, employee e, eref er) 
  11. {
  12.   /* requires getERef(t^, e) = erefNIL; */
  13.   modifies t;
  14.   /* ensures t' = add(t^, e, er); */
  15. }
  16.  
  17. bool ereftab_delete(ereftab t, eref er) 
  18. {
  19.   modifies t;
  20.   /* ensures result = in(t^, er) /\ t' = delete(t^, er); */
  21. }
  22.  
  23. eref ereftab_lookup(employee e, ereftab t) 
  24. {
  25.   /* ensures result = getERef(t^, e); */
  26. }
  27.  
  28. void ereftab_initMod(void) 
  29. {
  30.   modifies internalState;
  31.   ensures true;
  32. }
  33.  
  34. iter ereftab_elements(ereftab s, yield eref x);
  35.  
  36.  
  37.