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