Specification and Program Synthesis

Research into the development of software tools that support formal methods is aimed at simplifying and providing assistance during the development of correct software. Using a formal specification language to describe a problem facilitates the verification of the correctness of implemented software using automated reasoning techniques. In the SEED (SEmantic EDitor) project, we have shown that the building blocks of a complex software system can be correctly synthesized from user-supplied formal specifications. SEED accepts a predicate logic specification of a problem and generates program source code satisfying the specification. SEED's synthesis rules develop a program and its proof of correctness simultaneously.

The initial version of SEED synthesized primitive programming structures found in an imperative language, such as assignment, alternative, and iterative statements. Later versions of SEED supported procedural and data abstraction. In order to handle procedural abstractions in the system, rules were developed to synthesize recursive and non-recursive procedures and functions from specifications, which can be invoked through procedure calls and referenced with respect to their specifications. A set of of rules were developed to synthesize abstract data types from specifications in order to support data abstraction.

Recent Papers

  • ``Applying Formal Methods in Automated Software Development,'' Journal of Computer and Software Engineering, vol.~2, no.~2, pp.~137--164, 1994.

  • ``Graphical Development Environment for Larch Shared and Interface Languages'' (Michele Morin and Betty H.C. Cheng), Michigan State University Technical Report, MSU-CPS-94-18 April 1994.

  • ``An Integrated Development Environment for Formal Specifications'' (with Michael R. Laux and Robert H. Bourdeau), Proc. of the IEEE 5th International Conference on Software Engineering and Knowledge Engineering, pp. 681--688, San Francisco, California, June 1993.

  • ``An Object-Oriented Toolkit for Constructing Specification Editors,'' (with Robert H. Bourdeau), Proc. 16th Annual International Computer Software and Applications Conference, 239--244, September 1992.

  • ``Synthesis of Procedural Abstractions from Formal Specifications,'' Proc. of The Fifteenth International COMPSAC'91: Computer Software and Applications Conference, pp. 149--154. Tokyo, Japan, September 1991.

  • ``Automated Synthesis of Data Abstractions,'' Proc. of Irvine Software Symposium, Irvine, California, June 1991.

  • ``Synthesis of Procedural and Data Abstractions,'' (Betty H.C. Cheng) Tech Report UIUCDCS-R-90-1631, (Ph.D. Thesis). University of Illinois, Urbana, IL, August 1990.

  • ``A Semantically Oriented Program Synthesis System,'' {\em Proc. Hawaii International Conference on System Sciences-22,'' (Betty H.C. Cheng and Simon M. Kaplan), pp. 85--94, Kona, Hawaii, January 1989.