1 imports employee, empset, <stdio>;
3 typedef struct{gender g; job j; int l; int h;} db_q;
4 typedef enum { DBS_OK, DBS_SALERR, DBS_GENDERERR, DBS_JOBERR,
5 DBS_DUPLERR, DBS_MISSERR } db_status;
6 spec immutable type db;
9 claims UniqueKeys (employee e1, employee e2) db d;
12 (e1 \in d\any /\ e2 \in d\any /\ e1.ssNum = e2.ssNum)
17 db_status db_hire (employee e) db d;
22 then d' = hire(e, d^) else d' = d^)
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
32 void db_uncheckedHire (employee e) db d;
34 /* requires e.gen \neq gender_ANY /\ e.j \neq job_ANY
35 /\ e.salary >= 0 /\ ~employed(d^, e.ssNum);
38 /* ensures d' = hire(e, d^); */
41 bool db_fire (int ssNum) db d; internalState;
43 modifies d, internalState;
44 /* ensures result = employed(d^, ssNum)
45 /\ d' = fire(d^, ssNum);
49 int db_query (db_q q, empset s) db d; internalState;
51 modifies s, internalState;
52 /* ensures s' = s^ \U query(d^, q)
53 /\ result = size(query(d^, q));
57 bool db_promote (int ssNum) db d;
61 result = (employed(d^, ssNum)
62 /\ find(d^, ssNum).j = NONMGR)
63 /\ (if result then d' = promote(d^, ssNum)
68 db_status db_setSalary (int ssNum, int sal) db d;
74 (if employed(d^, ssNum)
75 then (if sal < 0 then salERR else db_OK)
78 then d' = setSal(d^, ssNum, sal)
83 void db_print(void) db d; FILE *stdout;
88 \exists s:ioStream ((*stdout^)' = write((*stdout^)^, s) /\ isSprint(d^, s));
92 void db_initMod(void) db d; internalState;
94 modifies d, internalState;
95 /* ensures d' = new; */