University of Illinois Urbana-Champaign

Debugging Logic Programs Using Executable Specifications

Lee, Yuh-Jeng

This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.

Permalink

https://hdl.handle.net/2142/69603

Description

Title
Debugging Logic Programs Using Executable Specifications
Author(s)
Lee, Yuh-Jeng
Issue Date
1988
Doctoral Committee Chair(s)
Dershowitz, Nachum
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Abstract
  • 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.
Graduation Semester
1988
Type of Resource
text
Permalink
http://hdl.handle.net/2142/69603

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Dept. of Computer Science