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 / db1 / erc.lcl < prev    next >
Text File  |  1997-09-03  |  2KB  |  98 lines
  1. imports eref;
  2.  
  3. mutable type erc;
  4. mutable type ercIter;
  5.  
  6. erc erc_create(void) 
  7. {
  8.   /* ensures fresh(result) /\ result' = { }; */
  9. }
  10.  
  11. void erc_clear(erc c) 
  12. {
  13.   /* requires c^.activeIters = 0; */
  14.   modifies c;
  15.   /* ensures c' = { }; */
  16. }
  17.  
  18. void erc_insert(erc c, eref er) 
  19. {
  20.   /* requires c^.activeIters = 0 /\ er \neq erefNIL; */
  21.   modifies c;
  22.   /* ensures c' = [insert(er, c^.val), 0]; */
  23. }
  24.  
  25. bool erc_delete(erc c, eref er) 
  26. {
  27.   /* requires c^.activeIters = 0; */
  28.   modifies c;
  29.   /* ensures result = er \in c^.val
  30.      /\ c' = [delete(er, c^.val), 0]; */
  31. }
  32.  
  33. bool erc_member(eref er, erc c) 
  34. {
  35.   /* ensures result = er \in c^.val; */
  36. }
  37.  
  38. eref erc_choose(erc c) 
  39. {
  40.   /* requires size(c^.val) \neq 0; */
  41.   /* ensures result \in c^.val; */
  42. }
  43.  
  44. int erc_size(erc c) 
  45. {
  46.   /* ensures result = size(c^.val); */
  47. }
  48.  
  49. ercIter erc_iterStart(erc c) 
  50. {
  51.   modifies c;
  52.   /* ensures fresh(result) /\ result' = [c^.val, c]
  53.         /\ c' = startIter(c^);
  54.   */
  55. }
  56.  
  57. eref erc_yield(ercIter it) 
  58. {
  59.   modifies it; /* , it^.eObj */ 
  60.   /* ensures if it^.toYield \neq { }
  61.      then yielded(result, it^, it')
  62.        /\ (it^.eObj)' = (it^.eObj)^
  63.      else result = erefNIL /\ trashed(it)
  64.        /\ (it^.eObj)' = endIter((it^.eObj)^);
  65.  */
  66. }
  67.  
  68. void erc_iterFinal(ercIter it) 
  69. {
  70.   modifies it; /* , it^.eObj; */
  71.   /* ensures trashed(it)
  72.      /\ (it^.eObj)' = endIter((it^.eObj)^);
  73.   */
  74. }
  75.  
  76. void erc_join(erc c1, erc c2) 
  77. {
  78.   /* requires c1^.activeIters = 0; */
  79.   modifies c1;
  80.   /* ensures c1' = [c1^.val \U c2^.val, 0]; */
  81. }
  82.  
  83. char *erc_sprint(erc c) 
  84. {
  85.   /* ensures isSprint(result[]', c^) /\ fresh(result[]); */
  86. }
  87.  
  88. void erc_final(erc c) 
  89. {
  90.   modifies c;
  91.   /* ensures trashed(c); */
  92. }
  93.  
  94. void erc_initMod(void) 
  95. {
  96.   ensures true;
  97. }
  98.