1imports employee, empset, <stdio>;
2
3typedef struct{gender g; job j; int l; int h;} db_q;
4typedef enum { DBS_OK, DBS_SALERR, DBS_GENDERERR, DBS_JOBERR,
5               DBS_DUPLERR, DBS_MISSERR } db_status;
6spec immutable type db;
7spec db d;
8
9claims UniqueKeys (employee e1, employee e2) db d;
10{
11 /* ensures
12     (e1 \in d\any /\ e2 \in d\any  /\ e1.ssNum = e2.ssNum)
13       => (e1 = e2);
14 */
15}
16
17db_status db_hire (employee e) db d;
18{
19  modifies d;
20  /* ensures
21     (if result = db_OK
22      then d' = hire(e, d^) else d' = d^)
23        /\ result =
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
28           else db_OK);
29  */
30}
31
32void db_uncheckedHire (employee e) db d;
33{
34  /* requires e.gen \neq gender_ANY /\ e.j \neq job_ANY
35            /\ e.salary >= 0 /\ ~employed(d^, e.ssNum);
36  */
37  modifies d;
38  /* ensures d' = hire(e, d^); */
39}
40
41bool db_fire (int ssNum) db d; internalState;
42{
43  modifies d, internalState;
44  /* ensures result = employed(d^, ssNum)
45       /\ d' = fire(d^, ssNum);
46  */
47}
48
49int db_query (db_q q, empset s) db d; internalState;
50{
51  modifies s, internalState;
52  /* ensures s' = s^ \U query(d^, q)
53       /\ result = size(query(d^, q));
54  */
55}
56
57bool db_promote (int ssNum) db d;
58{
59  modifies d;
60  /* ensures
61       result = (employed(d^, ssNum)
62                /\ find(d^, ssNum).j = NONMGR)
63          /\ (if result then d' = promote(d^, ssNum)
64              else d' = d^);
65  */
66}
67
68db_status db_setSalary (int ssNum, int sal) db d;
69{
70  modifies d;
71  /*
72  ensures
73      result =
74        (if employed(d^, ssNum)
75           then (if sal < 0 then salERR else db_OK)
76           else missERR)
77      /\ (if result = db_OK
78            then d' = setSal(d^, ssNum, sal)
79            else d' = d^);
80  */
81}
82
83void db_print(void) db d; FILE *stdout;
84{
85  modifies *stdout^;
86  /*
87  ensures
88    \exists s:ioStream ((*stdout^)' = write((*stdout^)^, s) /\ isSprint(d^, s));
89  */
90}
91
92void db_initMod(void) db d; internalState;
93{
94  modifies d, internalState;
95  /* ensures d' = new; */
96}
97
98