Programmable Messaging for Electronic Government - Building a Foundation - Formal Methods and Hybrid Real-Time Systems - page 229

6. unsubscribe - The function takes two identifiers as arguments - a channel
variable and a subscriber to this channel, and removes the id -category part
with the subscriber value from the variable. The precondition says that the
variable exists in the state and it contains a part representing the subscriber.

value
unsubscribe: Id × Id × State → StateX
unsubscribe(cid, mid, s) ≡
change(cid, del(idCat, id2val(mid), get(cid)))
pre eval(canUnsubscribe(cid, mid), s),
canUnsubscribe: Id × Id → BoolX
canUnsubscribe(cid, mid) ≡
let
x1 = hasVar(get(cid)),
x2 = hasPart(make(idCat, id2val(mid)), get(cid))
in and(x1, x2) end

4.6 Messaging

Messaging takes place by registered members exchanging messages along dy-
namically created and subscribed channels. Below we define three functions to
send messages - a message is put into the inbox of the sender, receive message -
a message is removed from the outbox of the recipient, and deliver messages - a
message is moved from the inbox of the sender to the outbox of all recipients.

7. send - The function takes two arguments - the identifier of the sender and
the message to be sent, and adds the message to the inbox of the sender. To
this end, the message is first converted into a value throught the mes2value
function, then this value is inserted into the inbox variable as a new mesCat -
category part. The precondition check that the sender is properly recorded
inside the message structure (equals to the value of the second id -category
part), that the address variable (identified by the third id -category part)
exists in the state, and that the sender of the message is identified in one of
this variable's id -category parts.

value
send: Id × Mes × State ∼ → StateX

send(mid, m, s) ≡

let x = make(mesCat, mes2val(m))
in change(inb(mid), add(x, get(inb(mid)))) end
pre eval(canSend(mid, m), s),
canSend: Id × Mes → BoolX
canSend(mid, m) ≡
let cid = val2id(val(m(idCat)(3)))
in and(hasVar(get(cid)), hasPart(make(idCat, id2val(mid)), get(cid))) end