Specialization of Recursive Predicates from Positive Examples Only
DOI : 10.3844/jcssp.2010.641.647
Journal of Computer Science
Volume 6, Issue 6
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.
© 2010 Moussa Demba. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.