Association of properties to definitions
This module implements the technique of deferred property
Many languages have constructs that define an identifier to denote
the same object as another, different identifier does.
Properties accessed or set via the one key should yield the same
results or effects as if the other key was used.
Typical examples for such constructs are type definitions
or constant definitions.
The module is instantiated by
$/Type/Defer.gnrc +referto=KEY :inst
referto parameter modifies the names
Key attributes, and hence, has to be the same as the
referto parameter used for the module instance that supplied
The roles of this module relate keys to each other which represent
the same object. That relation has to be acyclic. The properties
are associated to the keys at the ends of those relation chains.
A function is provided that walks down the chain when accessing
a property from any of the related keys.
This technique also decouples the computations which establish
the equivalence between keys from those which associate properties
to keys. It avoids cyclic dependencies between computations
in cases where properties of entities may be defined recursively,
e.g. recursively defined types.
Defer implements the relation between keys described
here. It should not be set otherwise than by using the
SetDeferId role of this module.
Setting a property to a key that may be an end of a
chain should occur in the context of the
If properties are accessed for a key
k that may be
Defer chain, the result of the call
TransDefer (k) has to be used instead of the
k itself, e.g.
GetKind (TransDefer (k), NoKind).
This module uses the
(See Some Useful PDL Specifications of Association of properties to definitions,) to obtain the
The module provides the following computational roles:
is a role for a defining occurrence of an identifier.
It establishes the
Defer relation from
SetDeferId.|KEY|Key to point to
A lower or upper computation for
THIS.DeferredKey has to be
An attempt to complete a
Defer cycle is not executed.
ChkSetDeferId is a role that may be inherited
by any identifier occurrence.
It checks whether an attempt was made to complete
Defer cycle involving this key.
The role should be inherited together with
Defer cycles are not otherwise excluded.
is a role that characterizes a context where properties may be
set to a key at the end of a
Computations that associate the properties have to
establish the postcondition represented by the
The role provides a default computation for
SYNT.GotDeferProp that states the empty postcondition.
is inherited by the grammar root by default.