next up previous contents index
Next: Artificial Intelligence Up: Research Topics Previous: Theorem Proving

Program Synthesis


The system acts as a program synthesizer in the following sense. Given a computationally meaningful assertion (e.g., a ``program specification''  ) and an applicable proof tactic which produces at least the executable parts of a proof of the assertion, the extractor  will produce from the proof a program. If the proof is complete then the program meets the specification. In this sense we have written a variety of program--synthesizing tactics. Several interesting comparisons can be drawn between these techniques and those based on classical methods, as in [Manna & Waldinger 80,Manna & Waldinger 85].

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995