APT (Automated Program Transformations) is a library of tools to transform programs and program specifications with automated support.

The APT transformation tools operate on ACL2 artifacts (e.g. functions) and generate corresponding transformed artifacts along with theorems asserting the relationship (e.g. equivalence) between old and new artifacts. The APT transformation tools modify the ACL2 state only by submitting sound and conservative events; they cannot introduce unsoundness or inconsistency on their own.

APT can be used in *program synthesis*,
to derive provably correct implementations from formal specifications
via sequences of refinement steps carried out via transformations.
The specifications may be declarative or executable.
The APT transformations can
synthesize executable implementations from declarative specifications,
as well as optimize executable specifications or implementations.
The APT transformations can also be used
to generate a variety of diverse implementations
of the same specification.

APT can also be used in *program analysis*,
to help verify existing programs, suitably embedded in the ACL2 logic,
by raising their level of abstraction via transformations
that are inverses of the ones used in stepwise program refinement.
The formal gap between a program and its specification
can be bridged by applying
top-down transformations to the specification
and bottom-up transformations to the code,
until they ``meet in the middle''.

APT enables the user to focus on the creative parts of the program synthesis or analysis process, leaving the more mechanical parts to the automation provided by the tools. The user guides the process by choosing which transformation to apply at each point and by supplying key theorems (e.g. applicability conditions of transformations), while APT takes care of the lower-level, error-prone details with speed and assurance.

The

Also see the APT Project Web page.

- Simplify-defun
- Simplify the definition of a given function.
- Isodata
- APT isomorphic data transformation: change function arguments and results into isomorphic representations.
- Tailrec
- APT tail recursion transformation: turn a recursive function that is not tail-recursive into an equivalent tail-recursive function.
- Schemalg
- APT schematic algorithm transformation: refine a specification by constraining a function to have a certain algorithmic form.
- Restrict
- APT domain restriction transformation: restrict the effective domain of a function.
- Expdata
- APT expanded data transformation: change function arguments and results into expanded representations.
- Casesplit
- APT case splitting transformation: rephrase a function definition by cases.
- Simplify-term
- Simplify a term.
- Simplify-defun-sk
- Simplify the definition of a given function made with
`defun-sk`. - Parteval
- APT partial evaluation transformation: specialize a function by setting one or more parameters to specified constant values.
- Solve
- APT solving transformation: directly determine a solution to a specification.
- Wrap-output
- Push an external computation into a function (by pushing it through the top-level if-branches of the function).
- Propagate-iso
- Propagate an isomorphism from a set of isomorphically transformed functions to events that use them.
- Simplify
- Simplify the definition of a given function.
- Finite-difference
- This transformation performs finite-differencing, aka incrementalization.
- Drop-irrelevant-params
- Removes some irrelevant parameters from a function.
- Copy-function
- Make a copy of a function, with recursive calls appropriately renamed.
- Lift-iso
- Lift an isomorphism to an isomorphism on a structure containing the original isoporphism predicate.
- Rename-params
- Rename one or more parameters in a function.
- Utilities
- Utilities shared by the implementations of the APT tools.
- Simplify-term-programmatic
- Programmatic interface to
`simplify-term` - Simplify-defun-sk-programmatic
- Programmatic interface to
`simplify-defun-sk` - Simplify-defun-programmatic
- Programmatic interface to
`simplify-defun` - Simplify-defun+
- Simplify the definition of a given function, including the guard and measure.
- Common-options
- Options that are common to different APT transformations.
- Common-concepts
- Concepts that are common to different APT transformations.