Strategies of structural synthesis of programs and its extensions

Proof search for the structural synthesis of programs (SSP) - a deductive p rogram synthesis method which is suited for compositional programming in la rge and is in practical use in a number of programming environments is expl ained. SSP is based on a decidable logical calculus where complexity of the proof search is still PSPACE. This requires paying special attention to th e efficiency of search. The practice of application of SSP has given its se veral modifications and extensions. Besides the general case of SSP and its strategies, we present synthesis with independent subtasks, a number of he uristics used for speeding up the search and partial deduction in the frame work of SSP.