Several identifiers are reserved for use as keywords in Larch/C++. (See section 4.6 Identifiers, however, for a mechanism for using a Larch/C++ keyword as an identifier.) To be accurate, however, not all such identifiers are always recognized by Larch/C++ as keywords; only an always-keyword is recognized as a keyword everywhere.
keyword ::= term-only-keyword | stmt-exp-only-keyword
| always-keyword
The following keywords are only recognized as keywords
in places where a Larch/C++ predicate or term
(see section 6.1 Predicates) can appear.
Therefore, within a C++ statement or expression
each is recognized as an identifier.
(The keyword on, while not technically appearing within
a term, is treated the same way.)
term-only-keyword ::=fresh|informally|liberally|on|nothing|post|pre|redundantly|result|returns|self|then|thrown|throws|trashed|unchanged
The following keywords are not recognized as keywords within a Larch/C++ term or predicate; in such places they are recognized as identifiers. Outside of a term, they are recognized as keywords, and can thus be used as keywords within a C++ statement or expression.
stmt-exp-only-keyword ::=break|case|catch|const_cast|continue|default|delete|dynamic_cast|goto|new|reinterpret_cast|return|static_cast|switch|throw|try|typeid
The following keywords are recognized as keywords in every context.
That is, they are truly reserved words.
Note that the C++ keywords if, else, and for are used
differently within specification terms in Larch/C++ than in C++.
always-keyword ::=abstract|accesses|also|any|asm|assert|assume|auto|behavior|be|by|calls|char|choose|class|constraint|constructs|const|decreasing|depends|double|do|else|ensures|enum|everything|example|expects|explicit|extern|float|for|friend|if|inline|int|invariant|is|let|long|maintaining|modifies|mutable|namespace|operator|or|private|program|protected|public|reach|refine|register|represents|requires|satisfies|short|signature|signed|simulates|sizeof|spec|static|struct|template|this|throw|trashes|typedef|typename|union|unsigned|uses|using|virtual|void|volatile|wchar_t|weakly|where|while|with
See section 4.15 Alternative Tokens, for other reserved words, used to support limited character sets.
Go to the first, previous, next, last section, table of contents.