Go to the first, previous, next, last section, table of contents.
An id, or identifier, is an expression which references an
object. Objects are instances of modules, variables, and defined
symbols. The syntax of an identifier is as follows.
id ::
atom
| "self"
| id "." atom
| id "[" simple_expr "]"
An atom identifies the object of that name as defined in a
VAR or DEFINE declaration. If a identifies an
instance of a module, then the expression `a.b' identifies
the component object named `b' of instance `a'. This
is precisely analogous to accessing a component of a structured data
type. Note that an actual parameter of module `a' can
identify another module instance `b', allowing `a'
to access components of `b', as in the following example:
... VAR a : foo(b); b : bar(a); ... MODULE foo(x) DEFINE c := x.p | x.q; MODULE bar(x) VAR p : boolean; q : boolean;
Here, the value of `c' is the logical or of `p' and `q'.
If `a' identifies an array, the expression `a[b]' identifies element `b' of array `a'. It is an error for the expression `b' to evaluate to a number outside the subscript bounds of array `a', or to a symbolic value.
It is possible to refer the name the current module has been
instantiated to by using the self builtin identifier.
MODULE element(above, below, token) VAR Token : boolean; ASSIGN init(Token) := token; next(Token) := token-in; DEFINE above.token-in := Token; grant-out := below.grant-out; MODULE cell VAR e2 : element(self, e1, 0); e1 : element(e1 , self, 1); DEFINE e1.token-in := token-in; grant-out := grant-in & !e1.grant-out; MODULE main VAR c1 : cell;
In this example the name the cell module has been instantiated to
is passed to the submodule element. In the main module,
declaring c1 to be an instance of module cell and defining
above.token-in in module e2, really amounts to defining
the symbol c1.token-in. When you, in the cell module,
declare e1 to be an instance of module element, and you
define grant-out in module e1 to be
below.grant-out, you are really defining it to be the symbol
c1.grant-out.