Debugging Logic Programs Using Executable Specifications

152 p.Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1988.This dissertation addresses the use of executable specifications in debugging logic programs which are renowned for their clean syntax and well-understood semantics, and for the feature that one can use a single language for both specification and computation. We have formulated a computer model that encodes programming knowledge including a classification of program bugs, heuristics that analyze and repair program errors, and operational semantics of the language, and utilizes deductive and inductive inference strategies to reason with programs and their specifications.The realization of our methodology is the Constructive Interpreter which functions as a debugger as well as a program synthesizer. It contains three major components: test case generator, bug locator, and bug corrector. When supplied with a program and its executable specifications, the test case generator can generate test data systematically by executing specifications. The Constructive Interpreter then executes the program on the test data. Should the execution fail to return an answer that agrees with the specifications, the bug locator will automatically locate a bug that is causing the failure. The bug corrector then analyzes the nature of the bug and utilizes correction heuristics which guide the use of the specifications and which attempt to repair the bug. This bug fixing process might involve the use of (1) a deductive theorem prover which will try to construct a proof and deduce sufficient conditions to amend the program, and (2) an inductive program generator which will synthesize the missing part of the program.U of I OnlyRestricted to the U of I community idenfinitely during batch ingest of legacy ETD