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 / employee.lcl < prev    next >
Text File  |  1997-09-03  |  1KB  |  55 lines
  1. imports <stdio> ;
  2.  
  3. constant size_t maxEmployeeName;
  4. constant int employeePrintSize;
  5.  
  6. typedef enum { MALE, FEMALE, gender_ANY } gender;
  7. typedef enum { MGR, NONMGR, job_ANY } job;
  8.  
  9. typedef struct 
  10. {
  11.   int ssNum;
  12.   char name[maxEmployeeName];
  13.   int salary;
  14.   gender gen;
  15.   job j;
  16. } employee;
  17.  
  18. void employee_sprint (out char s[], employee e) 
  19. {
  20.   /* requires maxIndex(s) >= employeePrintSize; */
  21.   modifies s;
  22.   /* ensures isSprint(s', e)
  23.         /\ lenStr(s') = employeePrintSize;
  24.   */
  25. }
  26.  
  27. bool employee_equal (employee *e1, employee *e2) 
  28. {
  29.   /* ensures result = sameStr(e1->name^, e2->name^)
  30.            /\ (e1->ssNum^ = e2->ssNum^)
  31.            /\ (e1->salary^ = e2->salary^)
  32.            /\ (e1->gen^ = e2->gen^)
  33.            /\ (e1->j^ = e2->j^);
  34.   */
  35. }
  36.  
  37. bool employee_setName(employee *e, char na[]) 
  38. {
  39.   /* requires nullTerminated(na^); */
  40.   modifies e->name;
  41.   /* ensures result = lenStr(na^) < maxEmployeeName
  42.            /\ (if result
  43.                then sameStr(e->name', na^)
  44.                      /\ nullTerminated(e->name')
  45.                else e->name' = e->name^);
  46.   */
  47. }
  48.  
  49. void employee_initMod(void) 
  50. {
  51.   modifies internalState;
  52.   ensures true;
  53. }
  54.  
  55.