]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | imports <stdio> ; |
2 | ||
3 | constant size_t maxEmployeeName; | |
4 | constant int employeePrintSize; | |
5 | ||
6 | typedef enum { MALE, FEMALE, GENDER_UNKNOWN } gender; | |
7 | typedef enum { MGR, NONMGR, JOB_UNKNOWN } 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, unique 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) internalState; | |
50 | { | |
51 | modifies internalState; | |
52 | ensures true; | |
53 | } | |
54 |