ID ::= TOKEN-ID TOKEN-ID ::= TOKEN TOKEN ::= WORDS | SIGNS | DOT-WORDS SIMPLE-ID ::= WORDS
The internal structure of identifiers ID, used to identify sorts, operations, and predicates, is insignificant in the abstract syntax of basic many-sorted specifications. (ID is extended with compound identifiers, whose structure is significant, in connection with generic specifications in Section 6.2.)
In concrete syntax, an identifier may be written as a single token: a sequence of letters and/or digits--possibly mixed with single underscores (_) and/or primes ('), and possibly prefixed by a dot (.)--or a sequence of other printable ISO Latin-1 characters (excluding ( ) ; , ` " %). Keywords, and various other sequences that could be confused with separators, are not allowed as tokens in the input syntax (however, display annotations may be used to produce them when formatting identifiers).
ID ::= ... | MIXFIX-ID MIXFIX-ID ::= mixfix-id TOKEN-OR-PLACE+ TOKEN-OR-PLACE ::= TOKEN | PLACE
An identifier may also be written as a mixfix identifier consisting of a list of tokens interspersed with place-holders. Mixfix identifiers allow the use of mixfix notation4 for applications of operations and predicates to argument terms in concrete syntax. The place-holders are written as pairs of underscores `__':
t0__...__tn`Invisible' identifiers, consisting entirely of two or more place-holders (separated by spaces), are allowed. Occurrences of `{...}' and of `[...]' in an identifier must be balanced; e.g., `{[__}]' and `{__]' are not allowed. Note that the brackets `[...]' are also used for writing compound identifiers in structured specifications, so declaring the mixfix symbol `__[__]' may give rise to ambiguity.
An identifier ID may be used simultaneously to identify different kinds of entities (sorts, operations, and predicates) in the same local environment. It should not, however, be used simultaneously for constants and variables of the same sort, since its (unqualified) use would then always be ambiguous, making the enclosing formula ill-formed.