Higher-Order and Symbolic Computation, 15(1/2)63-92
Program Synthesis from Formal Requirements Specifications Using APTSElizabeth I. Leonard, Naval Research Laboratory, Code 5546, Washington, DC 20375, USA
Constance L. Heitmeyer, Naval Research Laboratory, Code 5546, Washington, DC 20375, USA.
|
Abstract: Formal specifications of software systems are
extremely useful because they can be rigorously analyzed, verified,
and validated, giving high confidence that the specification captures
the desired behavior. To transfer this confidence to the actual source
code implementation, a formal link is needed between the specification
and the implementation. Generating the implementation directly from
the specification provides one such link. A program transformation
system such as Paige's APTS can be useful in developing a source code
generator. This paper describes a case study in which APTS was used to
produce code generators that construct C source code from a
requirements specification in the SCR (Software Cost Reduction)
tabular notation. In the study, two different code generation
strategies were explored. The first strategy uses rewrite rules to
transform the parse tree of an SCR specification into a parse tree for
the corresponding C code. The second strategy associates a relation
with each node of the specification parse tree. Each member of this
relation acts as an attribute, holding the C code corresponding to the
tree at the associated node; the root of the tree has the entire C
program as its member of the relation. This paper describes the two
code generators supported by APTS, how each was used to synthesize
code for two example SCR requirements specifications, and what was
learned about APTS from these implementations.
Keywords: code generation, code synthesis, APTS, SCR, requirements specifications, formal specifications, program transformation |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)