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

Below we define two functions to register and unregister members. Both func-
tions generate StateX expressions, with preconditions expressed at BoolX ex-
pressions, according to the definitions in Section 4.2. The execution of both
expressions is carried out through the corresponding eval functions.

1. register - The function carries out three operations concurrently: adding
aparttothe reg variable to identify a new member and declaring two
bType -type variables - inbox and outbox - for the member. The precondition
requires that the identifier of the new member does not belong to reg .

value
register: Id × State → StateX
register(id, s) ≡
let
x1 = make(new(inb(id), bType, id)),
x2 = make(new(outb(id), bType, id)),
x3 = change(id, add(make(idCat, id2val(id)), get(reg)))
in con(x3, con(decl(x1), decl(x2))) end pre eval(canRegister(id), s),
canRegister: Id BoolX

canRegister(id) ≡ not(hasPart(make(idCat, id2val(id)), get(reg)))

→

2. unregister - The function carries out three operations concurrently: unde-
clares two bType -type variables of the unregistered member, and deletes the
member's id-category part from the reg variable. The precondition checks
that the reg variable contains the part that identifies the member, and the
two bType -type variables for the member exist in the state.

value
unregister: Id × State → StateX
unregister(id, s) ≡

let
x1 = con(undecl(inb(id)), undecl(outb(id))),
x2 = change(id, del(idCat, id2val(id), get(reg)))
in con(x1, x2) end pre eval(canUnregister(id), s),
canUnregister: Id → BoolX
canUnregister(id) ≡
let
x1 = hasPart(make(idCat, id2val(id)), get(reg)),
x2 = and(hasVar(get(inb(id))), hasVar(get(outb(id))))
in and(x1, x2) end

4.5 Channels

Channels are represented as variables of the iType type. That is, every channel
variable contains identities of all members who are subscribers to this channel.
The owner of the channel variable is also the owner of the channel itself, respon-
sible for keeping the record of all subscribers. Below we define four functions to
create and destroy channels, and subscribe and unsubscribe to channels.