Keywords
The Java keywords [JLS14:3.9].
Some character sequences are Java keywords in all contexts,
namely the ones listed in the grammar production in [JLS14:3.9].
Other character sequences are Java keywords
only in certain module-related contexts,
as described in [JLS14:3.9] in prose (i.e. without grammar productions);
these are called `restricted keywords'.
To avoid conflict or confusion with ACL2 keywords,
we prefix keyword with j in ACL2 function and constant names
that pertain to Java keywords.
Subtopics
- Keywords-grammar-validation
- Validation of the definition of jkeywordp
with respect to the ABNF grammar of Java.
- Jkeywordp
- Recognize (non-restricted) Java keywords.
- Restricted-jkeywordp
- Recognize restricted Java keywords.
- *jkeywords*
- The (non-restricted) Java keywords, as ACL2 strings.
- *restricted-jkeywords*
- The restricted Java keywords, as ACL2 strings.
