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