An automatic debugging approach for logic programming with a method for propagating constraints

Focusing on logic programming, a practical method is proposed for verifying and debugging large programs invoking many subprograms. If a programmer gives a few simple constraints on arguments of the top-level program, then the approach automatically verifies that these constraints hold with a method for propagating constraints to its subprograms. Using both propagated constraints and recursive structure of programs, the method verifies the correctness of there constraints with an inductive method. Moreover, when these exists a constraint which can not hold, the approach shows debugging information on the program. The authors have implemented a verifying and debugging system for Prolog programs based on their method. Some experimental results are described