Methods for synthesizing predicate program pieces

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.