3 constant int maxEmployeeName;
4 constant int employeePrintSize;
6 typedef enum { MALE, FEMALE, gender_ANY } gender;
7 typedef enum { MGR, NONMGR, job_ANY } job;
12 char name[maxEmployeeName];
18 void employee_sprint (out char s[], employee e)
20 /* requires maxIndex(s) >= employeePrintSize; */
22 /* ensures isSprint(s', e)
23 /\ lenStr(s') = employeePrintSize;
27 bool employee_equal (employee *e1, employee *e2)
29 /* ensures result = sameStr(e1->name^, e2->name^)
30 /\ (e1->ssNum^ = e2->ssNum^)
31 /\ (e1->salary^ = e2->salary^)
32 /\ (e1->gen^ = e2->gen^)
37 bool employee_setName(employee *e, char na[])
39 /* requires nullTerminated(na^); */
41 /* ensures result = lenStr(na^) < maxEmployeeName
43 then sameStr(e->name', na^)
44 /\ nullTerminated(e->name')
45 else e->name' = e->name^);
49 void employee_initMod(void)