|
|
|---|
|
|
|
|---|
ATJ tutorial.
This is the top page of the ATJ tutorial.
This tutorial is work in progress, but it may be already useful in its current incomplete form. This tutorial's goal is to provide user-level information on how ATJ works and how to use ATJ effectively. See the ATJ manual page for the ATJ reference documentation, which currently contains some additional information that will likely be moved to this tutorial.
This tutorial consists of this top-level page plus a number of hyperlinked pages, all of which are subtopics of this top-level page, listed below alphabetically for easy reference. Starting from this top-level page, we provide Next links to navigate sequentially through all the tutorial pages (and we also provide Previous links going the opposite direction). It is recommended to follow this order when reading this tutorial for the first time. Each page starts with a short description of the contents of the page, and also says whether the page may be perhaps skipped at first reading, because it contains additional information that may not be necessary for a user to know in order to use ATJ. However, it is recommended to read all the tutorial pages, eventually.
This ACL2-2018 Workshop paper provides an overview of ATJ, but ATJ has been significantly extended since then. Some of the contents of the paper are being copied to this tutorial, and updated as appropriate; it is possible that the paper will be completely subsumed by this tutorial once the latter is completed.
Start: Motivation for Generating Java Code from ACL2