Algorithmic program diagnosis
Published 1 January 1982
Ehud Shapiro
Citations99
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
Algorithms for detecting incorrect procedures are developed and their performance suggests that the algorithms can be the backbone of debugging aids that go far beyond what is offered by current programming environments.
Abstract
The notion of program correctness with respect to an interpretation is defined for a class of programming languages. Under this definition, if a program terminates with an incorrect output then it contains an incorrect procedure. Algorithms for detecting incorrect procedures are developed. These algorithms formalize what experienced programmers may know already.A logic program implementation of these algorithms is described. Its performance suggests that the algorithms can be the backbone of debugging aids that go far beyond what is offered by current programming environments.Applications of algorithmic debugging to automatic program construction are explored.
Keywords
Computer Science
Information and ControlLanguage identification in the limit
3,569 Citations1967Eric Gold
It was found that theclass of context-sensitive languages is learnable from an informant, but that not even the class of regular languages is learningable from a text.
Negation as Failure
2,026 Citations1978Keith Clark
It is shown that when the clause data base and the queries satisfy certain constraints, which still leaves us with a data base more general than a conventional relational data base, the query evaluation process will find every answer that is a logical consequence of the completed data base.
Journal of the ACMThe Semantics of Predicate Logic as a Programming Language
1,463 Citations1976M. H. van Emden, Robert Kowalski
In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic are investigated, and it is concluded that operational semantics is a part ofProof theory and that fixpoint semantic is a special case of model-theoretic semantics.
Journal of the ACMA Transformation System for Developing Recursive Programs
1,316 Citations1977R. M. Burstall, John Darlington
A system of rules for transforming programs, with the programs in the form of recursion equations, are described, with an initially very simple, lucid, and hopefully correct program transformed into a more efficient one by altering the recursion structure.
Communications of the ACMProgram development by stepwise refinement
690 Citations1983Niklaus Wirth
The process of successive refinement of specifications is illustrated by a short but nontrivial example, from which a number of conclusions are drawn regarding the art and the instruction of programming.
Mathematical Theory of Computation
685 Citations1972Zohar Manna
This book is a classic text on sequential program verification; it has been widely translated from the original Hebrew and is much in demand among graduate students in the field of computer science.
ACM Computing SurveysProgramming in an Interactive Environment: the ``Lisp'' Experience
206 Citations1978Erik Sandewall
The paper summarazes the LISP style of interactive programming for readers outside the LisP community, describes those propertms of LisP systems that were essential for the development of this style, and discusses some current and not yet resolved issues.
IEEE Transactions on Software EngineeringSynthesis: Dreams → Programs
154 Citations1979Zohar Manna, Richard Waldinger
Deductive techniques are presented for deriving programs systematically from given specifications and have been incorporated in a running program-synthesis system, called DEDALUS.
Journal of the ACMDerivation of Logic Programs
130 Citations1981C. J. Hogger
Treating predicate logic as both a specification language and a programming language, firstorder logical deduction is shown to be sufficient for verifying, synthesizing, and transforming programs.
IEEE Transactions on Software EngineeringObservations of Fallibility in Applications of Modern Programming Methodologies
93 Citations1976S. Gerhart, L. Yelowitz
Errors, inconsistencies, or confusing points are noted in a variety of published algorithms, many of which are being used as examples in formulating or teaching principles of such modern programming methodologies as formal specification, systematic construction, and correctness proving.
An algorithm that infers theories from facts
63 Citations1981Ehud Shapiro
A framework for inductive inference in logic is presented, and it is shown that problems of machine learning and program synthesis from examples can be formulated naturally as model inference problems.
Lecture notes in computer scienceSelective backtracking for logic programs
18 Citations1980Luı́s Moniz Pereira, António Porto
A selective backtracking method for Horn clause programs, as applied to Prolog, a programming language based on first-order predicate calculus, developed at the university of Marseille.