]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | imports employee, empset, <stdio>; |
2 | ||
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; | |
7 | spec db d; | |
8 | ||
9 | claims 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 | ||
17 | db_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 | ||
32 | void 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 | ||
41 | bool 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 | ||
49 | int 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 | ||
57 | bool 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 | ||
68 | db_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 | ||
83 | void 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 | ||
92 | void db_initMod(void) db d; internalState; | |
93 | { | |
94 | modifies d, internalState; | |
95 | /* ensures d' = new; */ | |
96 | } | |
97 |