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

Formally, we define three abstract types to represent: identifiers Id ,values
Value and types Type , with initial value init , top-level type top and a subtype
relation sub defined between pairs of types. Several axioms are also defined to
constrain these values: sub is irreflexive, symmetric and transitive, and every
type is a subtype of top , except itself. Here is the self-explanatory model ex-
pressed in RSL - the RAISE Specification Language [21][22]:

type
Id, Value, Type
value
init: Value,
top: Type,
sub: Type × Type → Bool

axiom
( ∀ t: Type • t =top ⇒ sub(t, top)),
( ∀ t, t ,t :Type •
∼ sub(t, t) ∧
sub(t, t ) ∧ sub(t ,t) ⇒ t=t ∧
sub(t, t ) ∧ sub(t ,t ) ⇒ sub(t, t ))

Identifiers, types, messages, etc. can represent categories of parts, and can be
encoded as values, and back from values to original types. Here is the Cat type
with three values and a pair of symmetric functions for one of them:

type
Cat ==
idCat |
typeCat |
mesCat | ...

value
type2val: Type → Value,
val2type: Value → Type
axiom
( ∀ t: Type • val2type(type2val(t)) = t)

Lets define a type NatI of natural numbers with infinity, a type Cats of maps
from Cat to NatI , and a function (is smaller) that compares two maps if every

category in the first is also in the second, and the corresponding values in the
first map are not greater than in the second; inf is greater than any number. We
also define functions must and may to return mandatory and optional categories
for a given type, such as: n(0) is not in the range of may , inf is not in the range
of must , must is smaller than may for any type, may is smaller for a subtype than
for a supertype, and must is smaller for a supertype than for a subtype.

≤

type
NatI == inf | n(val: Nat ),
Cats = Cat

value
≤ :Cats × Cats → Bool
cs1 ≤ cs2 ≡
dom cs1 ⊆ dom cs2 ∧
( ∀ c: Cat • c ∈ dom cs1 ⇒
case (cs1(c), cs2(c)) of
(inf, ) → cs2(c) = inf,
( ,inf) → true ,
(n(n1), n(n2)) → n1 ≤ n2
end

m NatI

value
must,may:Type → Cats
axiom
( ∀ t: Type • must(t) ≤ may(t) ∧
n(0) ∈ rng may(t) ∧ inf ∈ rng must(t)

),
( ∀ t, t :Type • sub(t, t ) ⇒
may(t) ≤ may(t ) ∧ must(t ) ≤ must(t) )

)

The top type permits all categories in its may map, no number restriction
imposed, and requires two must categories: typeCat -therequiredtypeofa
structure and idCat - the identifier. These are mandatory for all types.