Paper Info
Title
Program Synthesis from Formal Requirements Specifications Using APTS
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.
Year
DOI
Venue
2003
10.1023/A:1023072104553
Higher-Order and Symbolic Computation
Keywords
Field
DocType
source code generator,scr,apts,code generator,different code generation strategy,scr specification,formal requirements,requirements specifications,example scr requirements specification,program synthesis,c source code,formal specifications,actual source code implementation,program transformation,code synthesis,parse tree,c code,corresponding c code,code generation,source code,computer programming,requirements,software systems,formal specification,software engineering
Parse tree,Programming language,Program synthesis,Source code,Computer science,Redundant code,Formal specification,Code generation,Software requirements specification,Computer programming
Journal
Volume
Issue
ISSN
16
1-2
1573-0557
Citations 
PageRank 
References 
17
0.80
24
Authors
2
Name
Order
Citations
PageRank
Elizabeth I. Leonard11108.48
Constance L. Heitmeyer2898151.71