|The key components of meta-programming used in this project
are abstract interpretation and partial evaluation, but related
techniques such as model checking and proof search are also employed.
Abstract interpretation is a semantically safe
technique for symbolically executing
programs, and partial evaluation is an automated program
transformation methodology; the two are combined into a program
transformer tool for symbolic execution of incomplete or component-based
programs. Importantly, the formal semantics of the ``symbols''
and their ``execution'' are supplied as inputs to the tool,
ensuring that the transformation steps taken on an input program
are semantically sound.
An incremental variant of abstract interpretation, called a
filter, lets one tune the symbolic execution to the
The tool is applied to individual program components. For each
component, the tool generates a finite-state abstraction that can
be model checked for validity or data-flow analyzed for synthesizing
an interface. Here, the novelty is that the finite-state model
is an incomplete component, yet it contains useful
Say that the issue at hand is validity of the component:
the ``gaps'' in the model (that is, the places where missing
components should be inserted) are instantiated with semantically sound
``stubs'' so that model-checking tools, such
as SPIN and SMV, can be used to check safety conditions.
If the goal is flow analysis of the component, a collecting-semantics
tool extracts data-flow information from the model and compresses it
into a residual, tabular form. The gaps in the model are encoded as
flow functions, which compute on the residual tables at link time.
Program components must be linked, and
the interface representations described
above---temporal logic formulas and compressed tables---must be linked
and computed upon further at link time.
Higher-order unification and proof search techniques
are used to synthesize linkage code for interfaces.