Apt
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 Community Books
currently contain only some APT transformations.
More transformations exist in Kestrel Institute's private files,
but they will be eventually moved to the Community Books.
Also see the APT Project Web page.
Subtopics
- 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.
