Java
An ACL2 library for Java.
Currently this library contains:
- A deep embedding of ACL2 in Java.
- A Java code generator for ACL2.
- A formalization in ACL2 of some aspects of the Java language.
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 `[JLS]' in the documentation of this library.
Chapters and sections are referenced
by appending their designations separated by colon,
e.g.
`[JLS:4.2]' references Section 4.2 of [JLS].
- The Java Virtual Machine specification, referenced as `[JVMS]' in the documentation of this library.
Chapters and sections are referenced
by appending their designations separated by colon,
e.g.
`[JVMS:5.5]' references Section 5.5 of [JVMS].
- The Java API specification, referenced as `[JAPIS]' in the documentation of this library.
These square-bracketed references may be used
as nouns or parenthentically.
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.
