		Search-engine friendly clone of the ACL2 documentation.

Java

Aij

AIJ (ACL2 In Java) is a deep embedding of ACL2 in Java.

AIJ is a deep embedding in Java of an executable, side-effect-free, non-stobj-accessing subset of the ACL2 language without guards.

AIJ is realized as a Java package that includes Java representations of all the ACL2 values, Java implementations of all the ACL2 primitive functions, and an interpreter that evaluates ACL2 translated terms to ACL2 values. The interpreter evaluates terms ``in the logic'', without checking guards and without side effects. The interpreter evaluates if non-strictly. The interpreter can be invoked only on (Java representations of) concrete ACL2 values, not on global variables like state and user-defined stobjs.

AIJ is in the java subdirectory of this directory, which contains an IntelliJ IDEA project. The Java code is thoroughly documented with Javadoc. AIJ is in a Java package called edu.kestrel.acl2.aij.

The Java source files of AIJ may be edited either in IntelliJ IDEA or in a text editor like Emacs. These source files can be compiled either in IntelliJ IDEA or via the Makefile file in this directory, which generates class and jar files in the same place where IntelliJ IDEA does. This Makefile also generates Javadoc HTML documentation.

AIJ is written in Java 8, which means that it can be compiled using a compiler for Java 8 or later. The aforementioned Makefile assumes that a Java 8 (or later) compiler and related tools (e.g. the latest OpenJDK) is in the path.

Subtopics

Aij-atj-paper: ACL2-2018 Workshop paper on AIJ and ATJ.