|
|
|---|
|
|
|
|---|
ATJ tutorial: Motivation for Generating Java Code from ACL2.
This tutorial page provides motivation for ATJ, and more in general for code generators for ACL2, especially in light of ACL2's code ability to run as Common Lisp code. This tutorial page may be skipped at first reading, especially if the reader is already motivated to generate Java code from ACL2.
A benefit of writing code in a theorem prover like ACL2 is the ability to prove properties about it, such as the satisfaction of requirements specifications. A facility to generate code in one or more programming languages from an executable subset of the prover's logical language enables the possibly verified code to run as, and interoperate with, code written in those programming languages. Assuming the correctness of code generation (whose verification is a separable problem, akin to compilation verification) the properties proved about the original code carry over to the generated code.
For instance, the Isabelle, Coq, PVS, and HOL theorem provers include facilities to generate code in various programming languages, such as SML, Ocaml, Haskell, Scala, C, and Scheme.
ACL2's tight integration with the underlying Lisp platform enables the executable subset of the ACL2 logical language to run readily and efficiently as Lisp, without the need for explicit code generation facilities. Nonetheless, some situations may call for running ACL2 code in other programming languages: specifically, when the ACL2 code must interoperate with external code in those programming languages in a more integrated and efficient way than afforded by inter-language communication via foreign function interfaces such as CFFI and JNI or by inter-process communication with the ACL2/Lisp runtime via mechanisms like the ACL2 Bridge. Using Lisp implementations written in the target programming languages, such as ABCL, involves not only porting ACL2 to them, but also including much more runtime code than necessary for the target applications. Compilers from Lisp to the target programming languages may need changes or wrappers, because executable ACL2 is not quite a subset of Lisp; furthermore, the ability to compile non-ACL2 Lisp code is an unnecessary complication as far as ACL2 compilation is concerned, making potential verification harder.
ATJ translates ACL2 to Java, enabling possibly verified ACL2 code to run as, and interoperate with, Java code, without much of the ACL2 framework or any of the Lisp runtime.
ATJ is useful to generate Java code at the end of an APT program synthesis derivation.
Generators for ACL2 of code in other programming languages (than Java) may be developed similarly to ATJ. An example is ATC, a C code generator for ACL2.