Geodesic
Methods for synthesizing predicate program pieces
Prikladnaya Diskretnaya Matematika. Supplement, no. 9 (2016), pp. 126-128.

Voir la notice de l'article provenant de la source Math-Net.Ru

In the predicate language $P$, a program is a set of computable predicates. The formal operational semantics of $P$ is developed. A total correctness formula for a predicate program with respect to its specification is presented on the base of the formal operational semantic. The synthesis problem for small pieces of a program in $P$ is considered. The synthesized program is defined as a composition of subprograms. Some synthesis rules are applied. The rules are developed on the base of the total correctness rules for deductive verification of the predicate programs. The synthesis problem for the predicate programs is clarified on the example program for an effective calculation of Fibonacci numbers. Some methods to synthesize functional programs are developed. These methods may be successfully used in developing the program synthesis methods starting from a program specification and the specifications of additional programs in a decomposition of the source program.
Keywords: formal operation semantics, program synthesis. 
@article{PDMA_2016_9_a49,
     author = {M. S. Chushkin and V. I. Shelekhov},
     title = {Methods for synthesizing predicate program pieces},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {126--128},
     publisher = {mathdoc},
     number = {9},
     year = {2016},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2016_9_a49/}
}
TY  - JOUR
AU  - M. S. Chushkin
AU  - V. I. Shelekhov
TI  - Methods for synthesizing predicate program pieces
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2016
SP  - 126
EP  - 128
IS  - 9
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2016_9_a49/
LA  - ru
ID  - PDMA_2016_9_a49
ER  - 
%0 Journal Article
%A M. S. Chushkin
%A V. I. Shelekhov
%T Methods for synthesizing predicate program pieces
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2016
%P 126-128
%N 9
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2016_9_a49/
%G ru
%F PDMA_2016_9_a49
M. S. Chushkin; V. I. Shelekhov. Methods for synthesizing predicate program pieces. Prikladnaya Diskretnaya Matematika. Supplement, no. 9 (2016), pp. 126-128. http://geodesic.mathdoc.fr/item/PDMA_2016_9_a49/

[1] Shelekhov V. I., “Semantika yazyka predikatnogo programmirovaniya”, 5-ya Vseros. konf. “Znaniya–Ontologii–Teorii”, IM SO RAN, Novosibirsk, 2015, 15

[2] Chushkin M. S., “Metody deduktivnoi verifikatsii predikatnykh programm”, Trudy 2-i Mezhdunar. konf. “Instrumenty i metody analiza programm”, Kostroma, 2014, 205–214

[3] Jacobs S., Kuncak V., Suter Ph., “Reductions for synthesis procedures”, Verification, Model Checking, and Abstract Interpretation, LNCS, 7337, 2013, 88–107 | MR

[4] Alur R., Bod'ik R., Juniwal G., et al., “Syntax-guided synthesis”, FMCAD, 2013, 1–8