Approaches to Automated Program Synthesis
Russian Federation, 119991, Moscow, GSP-1, Leninskie Gory, MSU, Computational Mathematics and Cybernetics faculty.2 pp. (accepted)
Nowadays computers are used in various domains, but in each of them solving a task on a computer means running a program, which implements a computational algorithm. But every practical task solving process starts not from programming itself, but from analysis of user's requirements: from the set of relations between the inputs and a result of a task. These conditions form a specification. We are going to explore how the programs can be constructed automatically from the given specifications. Two approaches are going to be exploited: the deductive synthesis and the case-based reasoning approach.
The deductive synthesis starts with a specification, which is taken as a mathematical existance theorem, and we need to prove it constructively. Each step of proof corresponds to a step of synthesis. The program derived using a deductive synthesis method doesn't require verification, because the derivation process contains the proof that the program corresponds to all the specified conditions. There are several methods for such program synthesis, but it is diffucult or even impossible to use them in the automatic mode on practice because of extremely large search space of proof attempts even for construction of simple programs. To solve the problem we propose to use proof planning, to combine different synthesis methods, to apply additional heuristics and to perfom parallel synthesis.
Case based reasoning represents another approach. For the domain of program synthesis each ”case” contains a specification and the corresponding program on some programming language. To derive a program from a specification we search for a similar speficication in the case library and adapt the corresponding solution. The correctness of the proposed solution is analysed by human or by an automated verification system.
Combining of different approaches to program synthesis helps to derive methods that allows ro perform automated synthesis on practice and enlarge the set of tasks for which the methods became useful.
1. Korukhova Y. An approach to automatic deductive synthesis of functional programs.// Annals of Mathematics and Artificial Intelligence, Vol. 50: 3-4 – Springer, 2007, p.255-271
2. Korukhova Y., Fastovets N. A Case-Based Reasoning Approach to Program Synthesis// Proceedings of The International Conference Knowledge Engineering and Ontology Development (KEOD), 2010.