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 / empset.lcl < prev    next >
Text File  |  1997-09-03  |  2KB  |  92 lines
  1. imports employee;
  2. mutable type empset;
  3.  
  4. only empset empset_create(void) 
  5. {
  6.   /* ensures fresh(result) /\ result' = { }; */
  7. }
  8.  
  9. void empset_final (only empset s) 
  10. {
  11.   modifies s;
  12.   /* ensures trashed(s); */
  13. }
  14.  
  15. void empset_clear(empset s) 
  16. {
  17.   modifies s;
  18.   /* ensures s' = { }; */
  19. }
  20.  
  21. | bool : void | empset_insert (empset s, employee e) internalState; 
  22. {
  23.   modifies s, internalState;
  24.   /* ensures result = ~(e \in s^) /\ s' = insert(e, s^); */
  25. }
  26.  
  27. void empset_insertUnique (empset s, employee e) internalState;
  28. {
  29.   /* requires ~(e \in s^); */
  30.   modifies s, internalState;
  31.   /* ensures s' = insert(e, s^); */
  32. }
  33.  
  34. | bool : void | empset_delete(empset s, employee e) 
  35. {
  36.   modifies s;
  37.   /* ensures result = e \in s^ /\ s' = delete(e, s^); */
  38. }
  39.  
  40. only empset empset_union(empset s1, empset s2) internalState;
  41. {
  42.   modifies internalState;
  43.   /* ensures result' = s1^ \U s2^ /\ fresh(result); */
  44. }
  45.  
  46. only empset empset_disjointUnion (empset s1, empset s2) internalState;
  47. {
  48.   modifies internalState;
  49.   /* requires s1^ \I s2^ = { }; */
  50.   /* ensures result' = s1^ \U s2^ /\ fresh(result); */
  51. }
  52.  
  53. void empset_intersect (empset s1, empset s2) internalState;
  54. {
  55.   modifies s1, internalState;
  56.   /* ensures s1' = s1^ \I s2^; */
  57. }
  58.  
  59. int empset_size(empset s) 
  60. {
  61.   /* ensures result = size(s^); */
  62. }
  63.  
  64. bool empset_member(employee e, empset s) 
  65. {
  66.   /* ensures result = e \in s^; */
  67. }
  68.  
  69. bool empset_subset(empset s1, empset s2) 
  70. {
  71.   /* ensures result = s1^ \subseteq s2^; */
  72. }
  73.  
  74. employee empset_choose(empset s) 
  75. {
  76.   /* requires s^ \neq { }; */
  77.   /* ensures result \in s^; */
  78. }
  79.  
  80. only char *empset_sprint(empset s) 
  81. {
  82.   /* ensures isSprint(result[]', s^) /\ fresh(result[]); */
  83. }
  84.  
  85. void empset_initMod (void) internalState;
  86. {
  87.   modifies internalState;
  88.   ensures true;
  89. }
  90.  
  91. iter empset_elements (empset s, yield employee x);
  92.