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 / dbase.lcl < prev    next >
Text File  |  1997-09-03  |  2KB  |  97 lines
  1. imports employee, empset, <stdio>;
  2.  
  3. typedef struct{gender g; job j; int l; int h;} db_q;
  4. typedef enum {db_OK, salERR, genderERR, jobERR,
  5.               duplERR, missERR} db_status;
  6. spec immutable type db;
  7. spec db d;
  8.  
  9. claims UniqueKeys (employee e1, employee e2) db d; 
  10. {    
  11.  /* ensures
  12.      (e1 \in d\any /\ e2 \in d\any  /\ e1.ssNum = e2.ssNum)
  13.        => (e1 = e2);
  14.  */
  15. }    
  16.  
  17. db_status hire(employee e) db d; 
  18. {
  19.   modifies d;
  20.   /* ensures
  21.      (if result = db_OK
  22.       then d' = hire(e, d^) else d' = d^)
  23.         /\ result =
  24.           (if e.gen = gender_ANY then genderERR
  25.            else if e.j = job_ANY then jobERR
  26.            else if e.salary < 0 then salERR
  27.            else if employed(d^, e.ssNum) then duplERR
  28.            else db_OK);
  29.   */
  30. }
  31.  
  32. void uncheckedHire(employee e) db d; 
  33. {
  34.   /* requires e.gen \neq gender_ANY /\ e.j \neq job_ANY
  35.             /\ e.salary >= 0 /\ ~employed(d^, e.ssNum);
  36.   */
  37.   modifies d;
  38.   /* ensures d' = hire(e, d^); */
  39. }
  40.  
  41. bool fire(int ssNum) db d; 
  42. {
  43.   modifies d;
  44.   /* ensures result = employed(d^, ssNum)
  45.        /\ d' = fire(d^, ssNum);
  46.   */
  47. }
  48.  
  49. int query(db_q q, empset s) db d; 
  50. {
  51.   modifies s;
  52.   /* ensures s' = s^ \U query(d^, q)
  53.        /\ result = size(query(d^, q));
  54.   */
  55. }
  56.  
  57. bool promote(int ssNum) db d; 
  58. {
  59.   modifies d;
  60.   /* ensures
  61.        result = (employed(d^, ssNum)
  62.                 /\ find(d^, ssNum).j = NONMGR)
  63.           /\ (if result then d' = promote(d^, ssNum)
  64.               else d' = d^);
  65.   */
  66. }
  67.  
  68. db_status setSalary(int ssNum, int sal) db d; 
  69. {
  70.   modifies d;
  71.   /* 
  72.   ensures
  73.       result =
  74.         (if employed(d^, ssNum)
  75.            then (if sal < 0 then salERR else db_OK)
  76.            else missERR)
  77.       /\ (if result = db_OK
  78.             then d' = setSal(d^, ssNum, sal)
  79.             else d' = d^);
  80.   */
  81. }
  82.  
  83. void db_print(void) db d; FILE *stdout; 
  84. {
  85.   modifies *stdout^;
  86.   /*
  87.   ensures 
  88.     \exists s:ioStream ((*stdout^)' = write((*stdout^)^, s) /\ isSprint(d^, s));
  89.   */
  90. }
  91.  
  92. void db_initMod(void) db d; 
  93. {
  94.   modifies d;
  95.   /* ensures d' = new; */
  96. }
  97.