Robert Harper. Proof-directed debugging. Journal of Functional Programming, 9(4):463-469, 1999.
Download paper:
Doi page
Download paper: (link)
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
The close relationship between writing programs and proving theorems has frequently been cited as an advantage of functional programming languages. We illustrate the interplay between programming and proving in the development of a program for regular expression matching. The presentation is inspired by Lakatos's method of proofs and refutations in which the attempt to prove a plausible conjecture leads to a revision not only of the proof, but of the theorem itself. We give a plausible implementation of a regular expression matcher that contains a flaw that is uncovered in an attempt to prove its correctness. The failure of the proof suggests a revision of the specification, rather than a change to the code. We then show that a program meeting the revised specification is nevertheless sufficient to solve the original problem
[ Regexp ]
@article{harper99,
Author = {Harper, Robert},
Title = {Proof-directed debugging},
Journal = {Journal of Functional Programming},
Volume = {9},
Number = {4},
Pages = {463--469},
Year = {1999}
}
Get EndNote Reference (.ref)