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

4.3 Messages

Just like a variable which is a structure valid with respect to the vType type,
a message is a structure which is valid with respect to the mType type. mType
requires all messages to contain at least one type-category part and at least three
id-category parts: message identifier, sender identifier and variable identifier. The
following type Mes represents all messages.

type
Mes = {| s: Struct • sub(sType(s), mType) |}
value
mType: Type • may(mType) = may(top) ∧
must(mType) = must(top) † [idCat → n(3) ]

The third required id-category part in a message identifies a variable that
contains the identities of all recipients of the message. These address variables
must have the type iType which requires precisely one type-category part and at
least two id-category parts: variable identifier, owner identifier and any number,
including zero, of member identifiers (recipients). If this number is zero, only the
owner (sender) will receive the message. In addition to iType , we also define the
type bType that requires zero or more parts of the mesCat category. Variables
of this type will hold lists of messages send and received by members.

value
iType: Type • may(iType) = [ typeCat → n(1), idCat → inf ] ...
bType: Type • may(bType) = [ typeCat → n(1), idCat → n(2), mesCat → inf ] ...

4.4 Members

Members are simply identified as the values of the type Id . Every variable in the
state must belong to exactly one member, identified through the value of the
second mandatory id-category part. A distinguished member, responsible among
others for registration of other members, is admin . admin owns the variable reg
that contains identities of all registered members. reg has the type iType just
like address variables. In addition, every member must have two bType -variables
to contain lists of incoming and outgoing messages for this member. Functions
inb and outb return the identifiers of these two message variables, uniquely
defined for every member identifier.

value
admin, reg: Id,
reg: Var •
val2id(val(reg(idCat)(1))) = reg ∧
val2id(val(reg(idCat)(2))) = admin ∧
sub(sType(reg), iType)

value
inb, outb: Id → Id
axiom
( ∀ id: Id • inb(id) = outb(id)) ∧
( ∀ id, id :Id • id =id ⇒

inb(id) =inb(id ) ∧
outb(id) = outb(id )
) ...