Atj-java-abstract-syntax
An abstract syntax of Java for ATJ's implementation.
This is not meant as a complete formalization
of an abstract syntax for Java.
It is just part of the implementation of ATJ,
and it suffices for that purpose,
namely that ATJ generates this abstract syntax
and then pretty-prints it to files.
This is why this abstract syntax is under kestrel/java/atj,
not under kestrel/java/language.
This abstract syntax may be eventually superseded
by a complete formalization under kestrel/java/language.
In fact, we have already started replacing some of this abstract syntax
with more complete counterparts from the language formalization,
namely the abstract syntax for integer literals.
The following remarks apply to this ATJ abstract syntax in general,
and so they are stated here instead of being repeated in several places:
- We do not capture annotations.
- We do not explicitly capture parameterized types, type variables, etc.
However, since we use arbitrary ACL2 strings for types,
< and > may be included as part of these strings.
- We use ACL2 strings and characters to capture Java strings and characters,
which is more restrictive because ACL2 characters are 8-bit,
while Java characters are 16-bit.
However, 8-bit characters suffice for ATJ's purposes,
which only generates ASCII Java code.
- We use ACL2 strings to capture
Java identifiers and dot-separated sequenced thereof.
On one hand, this is more restrictive
because of the 8-bit vs. 16-bit character issue;
on the other hand, it is more permissive
because it allows characters that are invalid for Java identifiers.
However, 8-bit characters suffice for ATJ's purposes,
which only generates ASCII Java code.
Furthermore, ATJ always does produce ACL2 strings
that are valid Java identifiers, or dot-separated sequences thereof.
Subtopics
- Jbinop
- Java binary operators [JLS14:15.17-24] [JLS14:15.26].
- Jmethod
- Java method declarations [JLS14:8.4].
- Jtype
- Java types [JLS14:4].
- Jfield
- Java field declarations [JLS14:8.3].
- Jexprs
- Java expressions [JLS14:15].
- Jliteral
- Java literals [JLS14:3.10].
- Junop
- Java unary operators [JLS14:15.15].
- Jlocvar
- Local variable declarations [JLS14:14.4].
- Jcunit
- Java compilation units [JLS14:7.3].
- Jaccess
- Java access modifiers [JLS14:8.1.1] [JLS14:8.3.1] [JLS14:8.4.3].
- Maybe-jexpr
- Java expressions or nil.
- Jparam
- Java formal parameter [JLS14:8.4.1].
- Jimport
- Java import declarations [JLS14:7.5].
- Jcinitializer
- Java class initializer [JLS14:8.6] [JLS14:8.7].
- Jresult
- Result of a Java method [JLS14:8.4.5].
- Jstatems+jblocks
- Java statements and blocks [JLS14:14].
- Jexpr-get-field
- Build a Java expression to access a field.
- Jliteral-long-dec-nouscores
- Build a Java long literal in base 10 without underscores.
- Nat-to-dec-chars-theorems
- Some theorems about str::nat-to-dec-chars
and the functions it calls.
- Jmethods-to-jcbody-elements
- Lift the composition of jcmember-method
followed by jcbody-element-member to lists.
- Jclasses-to-jcbody-elements
- Lift the composition of jcmember-class
followed by jcbody-element-member to lists.
- Jblock-locvar-final
- Build a block consisting of
a single final local variable declaration statement.
- Jblock-locvar
- Build a block consisting of
a single (non-final) local variable declaration statement.
- Jliteral-int-dec-nouscores
- Build a Java int literal in base 10 without underscores.
- Jfields-to-jcbody-elements
- Lift the composition of jcmember-field
followed by jcbody-element-member to lists.
- Jblock-for
- Bulid a block consisting of a single Java for statement.
- Jblock-smethod
- Build a block consisting of a single Java static method call.
- Jblock-imethod
- Build a block consisting of a single Java instance method call.
- Jblock-ifelse
- Build a block consisting of a single Java if-else statement.
- Jblock-asg-name
- Build a block consisting of a single Java assignment
where the left-hand side is a named expression.
- Jparam-list->types
- Lift jparam->type to lists.
- Jparam-list->names
- Lift jparam->name to lists.
- Jexpr-lit-long-dec-nouscores
- Build a Java expression consisting of
a long literal in base 10 without underscores.
- Jexpr-lit-int-dec-nouscores
- Build a Java expression consisting of
an int literal in base 10 without underscores.
- Jexpr-literal-string
- Build a Java expression consisting of a string literal.
- Jexpr-literal-floating
- Build a Java expression consisting of a floating-point literal.
- Jexpr-literal-character
- Build a Java expression consisting of a character literal.
- Jblock-while
- Build a block consisting of a single Java while statement.
- Jblock-method
- Build a block consisting of a single Java method call.
- Jblock-if
- Build a block consisting of a single Java if statement.
- Jblock-expr
- Build a block consisting of a single Java expression
(as an expression statement.
- Jblock-do
- Build a block consisting of a single Java do statement.
- Jblock-asg
- Build a block consisting of a single Java assignment.
- Jexpr-name-list
- Lift jexpr-name to lists.
- Jblock-throw
- Build a block consisting of a single Java throw statement.
- Jblock-return
- Build a block consisting of a single Java return statement.
- Jparam-list
- Lists of Java formal parameters.
- Jimport-list
- Lists of Java import declarations.
- Jexpr-literal-true
- Build a Java expression consisting of
the boolean literal true.
- Jexpr-literal-null
- Build a Java expression consisting of the null literal.
- Jexpr-literal-false
- Build a Java expression consisting of
the boolean literal false.
- Jexpr-literal-1
- Build a Java expression consisting of the integer literal 1.
- Jexpr-literal-0
- Build a Java expression consisting of the integer literal 0.
- Jclass-list
- Lists of Java class declarations.
- Jblock-continue
- Build a block consisting of a single Java continue statement.
- Jtype-short
- Build the Java primitive type short.
- Jtype-long
- Build the Java primitive type long.
- Jtype-list
- Lists of Java types.
- Jtype-int
- Build the Java primitive type int.
- Jtype-float
- Build the Java primitive type float.
- Jtype-double
- Build the Java primitive type double.
- Jtype-char
- Build the Java primitive type char.
- Jtype-byte
- Build the Java primitive type byte.
- Jtype-boolean
- Build the Java primitive type boolean.
- Jmethod-list
- Lists of Java method declarations.
- Jliteral-list
- Lists of Java literals.
- Jfield-list
- Lists of Java field declarations.
- Jblock-list
- Lists of Java blocks.
- Jblock-break
- Build a block consisting of a single Java break statement.
- Jclasses+jcmembers
