TY - GEN
T1 - Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs
AU - Hesketh, J.
AU - Bundy, Alan
AU - Smaill, A.
PY - 1992
Y1 - 1992
N2 - We describe a novel technique for the automatic synthesis of tail-recursive programs. The technique is to specify the required program using the standard equations and then synthesise the tail-recursive program using the proofs as programs technique. This requires the specification to be proved realisable in a constructive logic. Restrictions on the form of the proof ensure that the synthesised program is tail-recursive.The automatic search for a synthesis proof is controlled by proof plans, which are descriptions of the high-level structure of proofs of this kind. We have extended the known proof plans for inductive proofs by adding a new form of generalisation and by making greater use of middle-out reasoning. In middle-out reasoning we postpone decisions in the early part of the proof by the use of meta-variables which are instantiated, by unification, during later parts of the proof. Higher order unification is required, since these meta-variables can represent higher order objects.The program synthesised is automatically verified to ensure that it satisfies its specification. This type of verification is contrasted with template-based transformation approaches which require proofs that the general transformations described by the templates preserve equivalence.The technique described is more general than template-based approaches, since it is not tied to program patterns which must be specified in advance. Detailed information about proof structure enables it to use a wider repertoire of rewritings in a more goal-directed way than comparable transformational techniques.
AB - We describe a novel technique for the automatic synthesis of tail-recursive programs. The technique is to specify the required program using the standard equations and then synthesise the tail-recursive program using the proofs as programs technique. This requires the specification to be proved realisable in a constructive logic. Restrictions on the form of the proof ensure that the synthesised program is tail-recursive.The automatic search for a synthesis proof is controlled by proof plans, which are descriptions of the high-level structure of proofs of this kind. We have extended the known proof plans for inductive proofs by adding a new form of generalisation and by making greater use of middle-out reasoning. In middle-out reasoning we postpone decisions in the early part of the proof by the use of meta-variables which are instantiated, by unification, during later parts of the proof. Higher order unification is required, since these meta-variables can represent higher order objects.The program synthesised is automatically verified to ensure that it satisfies its specification. This type of verification is contrasted with template-based transformation approaches which require proofs that the general transformations described by the templates preserve equivalence.The technique described is more general than template-based approaches, since it is not tied to program patterns which must be specified in advance. Detailed information about proof structure enables it to use a wider repertoire of rewritings in a more goal-directed way than comparable transformational techniques.
U2 - 10.1007/3-540-55602-8_174
DO - 10.1007/3-540-55602-8_174
M3 - Conference contribution
SN - 978-3-540-55602-2
T3 - Lecture Notes in Computer Science
SP - 310
EP - 324
BT - Automated Deductionâ€”CADE-11
PB - Springer Berlin Heidelberg
ER -