-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMailBox.thy
85 lines (66 loc) · 3.77 KB
/
MailBox.thy
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
theory MailBox
imports "Z_Machines.Z_Machine"
begin
text \<open>An electronic mail system consists of several instances of the component MailBox. Each instance may be associated with one or more addresses from the set Address. A user of the system may have more than one address, and an address may be associated with more than one user.\<close>
subsection \<open> Types \<close>
type_synonym user = string
type_synonym address = string
type_synonym mailbox = string
type_synonym message = string
type_synonym timestamp = string
text \<open>We define the set of all users, address, and mialboxes.\<close>
consts
USER :: "user set"
ADDRESS :: "address set"
MAILBOX :: "mailbox set"
MESSAGE :: "message set"
TIMESTAMP :: "timestamp set"
subsection \<open> State Space \<close>
text \<open>3 variables are declared. mail is a sequence of type Message, representing the mail messages stored in the box.
new_mail records the time of arrival of the latest mail message, and last_read records the last time that mail in the box was read.\<close>
zstore MailBox =
mail :: "message list"
new_mail :: "timestamp"
last_read :: "timestamp"
text \<open>Global: The association between users and addresses is given by a relation address, and the association between addresses and the local mailboxes is given by the partial function mailbox\<close>
zstore MailSystem =
address :: "user \<leftrightarrow> address"
mailbox :: "address \<Zpfun> MailBox"
where "dom(mailbox) = ADDRESS"
subsection \<open> operations \<close>
text \<open>this local operation describes the effect of adding mail to a single mailbox.
The incoming message is added to the end of the sequence mail, and the new mail is set to t. The other time stamp last_read remains unchanged so omitted.\<close>
zoperation ReceiveBox =
over MailBox
\<comment>\<open>m and t are the two inputs to the operation\<close>
params m\<in>MESSAGE t\<in>TIMESTAMP
update "[mail\<Zprime> = mail @ [m]
, new_mail\<Zprime> = t
]"
text \<open>If a message m arrives at time t for user u, then it will be added to one of the mailboxes belonging to u.
a is provided as an output to the operation.
u, m, t are inputs\<close>
zoperation ReceiveSystem =
over MailSystem
params u\<in>USER a\<in>ADDRESS m\<in>MESSAGE t\<in>TIMESTAMP
pre "(a\<in> dom mailbox \<and> u \<in> dom address \<and> address(u) = a) "
update "[mailbox[a]:mail\<Zprime>= $mailbox[a]:mail @ [m]
, mailbox[a]:new_mail\<Zprime> = t
]"
def_consts USER = "{ ''Carolyn'', ''Denise'', ''Edward''}"
def_consts ADDRESS = "{ ''admin'', ''carolyn'', ''denise'', ''edward'', ''edwardc''}"
def_consts TIMESTAMP = "{''Tue 14 Feb, 11:00 a.m.'', ''Thur 16 Feb, 09:00 a.m.'', ''Tue 12 Mar, 09:50 a.m.'', ''Mon 18 Mar, 03 p.m.''}"
def_consts MESSAGE = "{''m1'', ''m2'', ''m3'', ''m4'', ''m5''}"
zmachine MailSystemProc =
over MailSystem
init "[address\<Zprime> = {''Carolyn'' \<mapsto> ''admin'', ''Carolyn'' \<mapsto> ''carolyn'', ''Denise'' \<mapsto> ''denise'', ''Denise'' \<mapsto>''admin'', ''Edward'' \<mapsto>''edward'', ''Edward'' \<mapsto>''edwardc''},
mailbox\<Zprime> = {
''admin'' \<mapsto> \<lblot>mail\<leadsto> [],new_mail \<leadsto>'' '', last_read\<leadsto> '' '' \<rblot>,
''carolyn'' \<mapsto>\<lblot>mail\<leadsto> [],new_mail \<leadsto>'' '', last_read\<leadsto> '' '' \<rblot>,
''denise'' \<mapsto> \<lblot>mail\<leadsto> [],new_mail \<leadsto>'' '', last_read\<leadsto> '' '' \<rblot>,
''edward'' \<mapsto> \<lblot>mail\<leadsto> [],new_mail \<leadsto>'' '', last_read\<leadsto> '' '' \<rblot>,
''edwardc'' \<mapsto>\<lblot>mail\<leadsto> [],new_mail \<leadsto>'' '', last_read\<leadsto> '' '' \<rblot>}
]"
operations ReceiveSystem
animate MailSystemProc
end