The synthesis tableau: a deductive framework for program synthesis based on sequent calculus
Talal Hamza Maghrabi · 1992
Modern engineering techniques aim at developing programs that are shorter, clearer and, above all, correct. The well-recognized software crisis is a symptom of the limitations inherent in the traditional approach to the specification, design, and programming of complex systems. Investigations into program correctness have led to the discovery of several novel and interesting methods for program development. The theorem proving approach for program synthesis is based on the idea that programs and their proof of correctness may be generated hand-in-hand within a rigorous formal framework. In this approach the specification of a desired program is stated as a well-formed formula (wff) in First Order Logic. A proof that this wff is a theorem in some theory is then conducted, from which the desired program is generated as a side effect. In this dissertation a mathematical framework that is based on the theorem proving approach is developed. This framework, called the synthesis tableau, unlike many of the current efforts in this area that use resolution, is based on sequent calculus. The synthesis tableau enables the user to use transformation rules, inference rules, and the induction rule in deriving both the proof of the given specification and the statements of the desired program. A simple prototype implementing the basic ideas of the synthesis tableau is also developed.