LOTOS uses ACT 1 to define a language for types and algebras,
so that variables and expressions may be included in a protocol
specification. ACT is an Abstract Data Type language, or Object
oriented language. This means that one specifies not only types
for variables, but also the set of operations allowed on these
types.
Typical specifications include:
-
sorts
The sorts of things we are defining
-
opns
The operations on these sort of things
-
sort
A sort identifier for use when defining variables of this sort.
-
eqns
Defining legal equations on these sorts of things.