A New Technique for Verifying and Correcting Logic Programs

摘要: A significant extension to a model-building method that we have been developing for several years is presented. quite complete, albeit reasonably short, description of the previous given in order make this article self-contained. The enables handling Presburger arithmetic and deducing inductive consequences from sets Horn clauses. For large class logic programs also permits deduction negative facts detection nontermination. It shown how extended can be used verifying correcting programs. proposed verifies w.r.t. formal specifications, but its fundamentals (i.e., model building) it useful pointing out errors suggesting way wrong informal such as specifications by examples or using implicit knowledge (the latter features are especially when dealing with beginners’ programs). Theoretical properties (e.g., soundness refutational completeness) proven. greater power extensions programming enabled our relative existing methods respect other standard (like negation failure) Several nontrivial illustrate error correction well broadening inference capabilities obtained rules method. These detailed show evidence interest approach. Main directions future research given.