Introduction to Deductive Synthesis
The deductive approach to program synthesis transforms program synthesis into a theorem-proving task. [Manna and Waldinger, Chapter 1] provides an introduction to the key ideas of this approach, namely the correspondence between theorems and specifications and between constructive proofs and programs. Manna and Waldinger have developed a logical framework specially suited to program synthesis and illustrate its use in a number of examples. Although this logic is ultimately intended for use in automatic synthesis systems, no implementation currently exists.
[Smith, Chapter 2] describes an implemented deductive synthesis system, called CYPRESS, based on a related, but slightly different, logical framework. ...
Get Readings in Artificial Intelligence and Software Engineering now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
