|
|
|---|
|
|
|
|---|
ATC tutorial: Comparison with ATJ's Java code generation from ACL2.
(This page may be skipped at first reading.)
ATC is related to ATJ, a Java code generator for ACL2. Aside from the obvious difference in target languages, ATJ and ATC currently differ in their primary goals and emphases.
ATJ is built to recognize, and translate to reasonable Java, essentially any ACL2 code (provided that it has side effects known to ATJ). ATJ also provides ways to exert finer-grained control on the generated Java, by using certain ACL2 types and operations that represent Java types and operations and that are translated to the corresponding Java constructs. While there are plans to have ATJ generate ACL2 proofs of the correctness of the generated code, ATJ currently does not generate proofs.
In contrast, ATC is built to recognize, and translate to C, only certain ACL2 types and operations that represent C types and operations and that are translated to the corresponding Java constructs. ATC does not attempt to translate arbitrary ACL2 to C. ATC also generates ACL2 proofs of the correctness of the generated C code.
The fact that ATC is simpler than ATJ facilitates the generation of proofs. Generating proofs for ATJ is a larger task, due to the greater complexity.
In the future, ATC may be extended towards recognizing any ACL2 code and translating it to reasonable C, analogously to ATJ; but the plan is for ATC to always generate proofs. Conversely, ATJ may be extended to generate proofs as well. Thus, while eventually ATJ and ATC may provide similar features, their starting points and tradeoffs are different, and that will keep the two tools different for some time to come.