Sketch completion for predicate programs by counterexamples guided synthesis

Predicate programs are presented in the language P by sets of computable predicates. For programs in P, the formal operational semantics is developed. On the base of this semantics, a formula describing the total correctness of a predicate program with respect to its specification is presented. The problem of sketch completion for programs in P is considered. The sketch of a program is defined as a typical program with arbitrary expressions. The idea of arbitrary expressions is inspired by the synthesis of programs by a sketching method. Arbitrary expressions are synthesized by counterexample guided synthesis method. The correctness formulas for completed programs are generated. Some methods to synthesize expressions are developed. These methods can be successfully used in our project instead of counterexample guided synthesis. The overall project objective is to develop the program synthesis methods starting from a program specification and the specification of additional programs used in the decomposition of the source program. The nearest project objective is to be able to synthesize elementary expressions in constructed programs.

Keywords

Authors

References