Automatic transformation of high-level logic specifications into high-performance target code

Development of software systems typically proceeds from informal user requirements through development of formal specifications which form the basis for detailed designs and implementations. Of these, implementation is the most involved, costly, and source of errors which require continuous maintenance throughout the software life-time. An additional source of errors is miscommunication between users who develop the informal requirements and designers and implementors who effect those requirements.;A methodology is proposed for formal specification and automatic generation of software systems, based upon the theory of Two-Level Grammar (TLG). TLG is developed into a complete specification language under the paradigms of functional and logic programming. TLG specifications are unique in that they are a structured form of natural language which is executable, greatly increasing the reliability of the developed software system for the following reasons. Because it is a form of natural language, TLG may be used as an effective communication medium between users, designers, and implementors of the system, thereby reducing errors caused by miscommunication. Furthermore, because TLG is implementable, we may automatically generate the software system from the specification in a provably correct way. This is accomplished by transforming the TLG high-level specifications into efficient target programs expressed in C. Our target programs are then compiled using widely-available C compilers, making them highly portable, and they may interface with many existing C programs, facilitating software reuse. Finally, the main advantage is that developing TLG specifications is considerably easier and less error-prone than developing C programs, where considerably more implementation detail is needed.;The effectiveness of our method is demonstrated through the automatic generation of: (1) a lazy functional language graph reduction implementation, (2) a semantics-directed compiler for a Pascal-like language, and (3) a database/knowledge-base management system based upon SQL. For the DBMS, we have the additional advantage that the TLG specification results in an embedding of SQL into TLG offering both deductive capabilities and expressive natural language queries. All the generated programs are comparable in time and space efficiency with corresponding C programs coded by hand and greatly improve upon interpretative and Prolog prototype versions of the TLG specifications.