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

For example, here is a function to add a part to a structure, by appending
it at the end of its category list. Like canDecl , canAdd is expressed through a
generated boolean expression BoolX , evaluated on the current state.

value
add: Part × Struct × State → Struct
add(p, st, s) ≡ st † [ cat(p) → st(cat(p)) ￿ p ] pre eval(canAdd(p, st), s),

canAdd: Part × Struct → BoolX
canAdd(p, st) ≡ and(
isMay(cat(p),make(st)),
isless(parts(make(st),cat(p)), may(make(st),cat(p))))

Similarly, we define types for other expressions. PartX includes operators to:
make a part from a category and a value expression, get a part from a structure
given a category and a number expression, and change the part value for given
value and part expressions. ValueX includes operators to: make values, get values
from parts, and obtain values from types, identifiers or messages. NatX includes
operators to: make numbers, get numbers from the state - number of variables,
number of categories in a structure, number of parts with a given category and
value, number of mandatory and permissible parts - add them, etc.

type
PartX ==
make(Cat, ValueX) |
get(StructX, Cat, NatX) |
change(ValueX, PartX)

type
ValueX ==
make(Value) |
get(PartX) |
id2val(Id) |
type2val(Type) |
mes2val(Mes)

type
NatX ==
make(NatI) | vars |
cats(StructX) |
parts(StructX, Cat) |
may(StructX, Cat) |
must(StructX, Cat) |
add(NatX, NatX)

Finally, the BoolX type contains a set of operators to make and combine
boolean values and to check: if a structure exists in the state; if a structure
contains parts of a given category; if a structure has a given type; if a given part is
contained in a structure; if the part contained in a structure has a given category
or value; if a value expression equals a given value; if a number expression equals
a given number; if one number expression is less than another; if one type is
a subtype of another; etc. We also present the signatures of eval functions for
PartX , ValueX , NatX and BoolX expressions.

type
BoolX ==
tt | not(BoolX) | and(BoolX, BoolX)
or(BoolX, BoolX) | hasParts(Cat, StructX) |
hasVar(StructX) | hasType(StructX, Type) |
hasPart(PartX, StructX) | hascVar(Id) |
hasCat(PartX, Cat) | hasVal(PartX, ValueX) |
isMay(Cat, StructX) | isMust(Cat, StructX) |
equal(ValueX, Value) | equal(NatX, NatI) |
isless(NatX, NatX) | issub(Type, Type)

value
eval: PartX × State → Part,
eval: ValueX × State → Value,
eval: NatX × State → NatI,
eval: BoolX State ∼ × → Bool