Java
An ACL2 library for Java.
Currently this library contains:
- A formalization in ACL2 of some aspects of the Java language.
- A deep embedding of ACL2 in Java.
- A Java code generator for ACL2.
It is expected that this library will be extended with more
Java-related formalizations and tools.
This library is based on the following sources:
- The Java language specification, referenced as `[JLSe]' in the documentation of this library,
where `e' is the Edition, e.g. `[JLS21]' for Java SE 21 Edition.
Chapters and sections are referenced
by appending their designations separated by colon,
e.g.
`[JLS21:4.2]' references Section 4.2 of [JLS21].
- The Java Virtual Machine specification, referenced as `[JVMSe]' in the documentation of this library,
where `e' is the Edition, e.g. `[JVMS21]' for Java SE 21 Edition.
Chapters and sections are referenced
by appending their designations separated by colon,
e.g. `[JVMS21:5.5]' references Section 5.5 of [JVMS21].
- The Java API specification, referenced as `[JAPISe]' in the documentation of this library
where `e' is the Edition, e.g. `[JAPIS21]' for Java SE 21 Edition.
These square-bracketed references may be used
as nouns or parenthentically.
The documentation of this library may use references
for different Java Editions, e.g. [JLS21] and [JLS20].
Ideally, all the references should be for the latest Edition,
but in practice it may take time to update them
when a new Java Edition is released (which happens relatively often);
the references need to be double-checked for each new Edition,
as things may change.
By always using the Edition number in the references,
we at least guarantee their accuracy.
Subtopics
- Atj
- ATJ (ACL2 To Java)
is a Java code generator for ACL2.
- Aij
- AIJ (ACL2 In Java)
is a deep embedding of ACL2 in Java.
- Language
- A formal model of some aspects of the Java language.
