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