Specialization of Recursive Predicates from Positive Examples Only

Problem statement: Given an overly general (definite) program P and its intended semantics Φ (the programmer’s intentions) where P does not satisfy Φ, find out a new version P’ of P such that P’ satisfies Φ. Approach: We proposed an approach for correcting overly general programs from positive examples by exploiting program synthesis techniques. The synthesized program, P’, is a specialization of the original one, P. In contrast to the previous approaches for logic program specialization, no negative examples were given as input but they will be discovered by the algorithm itself. The specialization process is performed according to the positive examples only. A method for refining logic programs into specialized version was then proposed. Results: The proposed approach was able to correct overly general programs using positive examples. We showed that positive examples can also be used for inducing finite-state machines, success sequences, that models the correct program. The failing sequences also exploited by theorem proved to produce counter-examples as in model checking, by composing substitutions used for inducing failing sequences. Conclusion: The contribution of the study was mainly the use of specification predicates to specialize an overly general logic program.