The Use of Proof in the Location of Programming Errors

Overview

The use of mathematical proof to show that a computer program meets its specification has a long history in Computer Science (e.g. [Naur 66, Morris and Jones 84]). Considerable time and effort has been invested by academics in creating computer-based tools to support the process of proving programs correct (e.g. [Paulson 94, Gordon and Melham 93]). However the technique and tools are only used in very specialised situations in industry where instead programmers generally rely on testing and responding to bug reports from users to assess the extent to which a program meets its specification. This has resulted in widespread problems with the reliability of computer systems. There are several reasons why there is such poor uptake of the use of proof in industry. One reason is that the final proof will tell you if the program is correct, but failing to find a proof does not apparently help in locating errors. Many cases have been reported where the process of attempting a proof by hand has highlighted an error, for instance Paulson's discovery of new attacks against security protocols [Paulson 98]. Anecdotal evidence suggests that errors are located by examining and reflecting on the process of the failed proof attempt. Another reason for the poor uptake is that such proofs can be very difficult and require experts to produce - this has led to a great deal of research into automating the proof process using computers (e.g. [Bundy 91]). Sadly, a downside of the automation process is that when a proof is not found virtually no information is available which can be used even as a starting point for locating errors - the program generally simply reporting that no proof was found.

This leads me to believe that we need a better understanding of the connection between bugs in programs and the failure of their correctness proofs. This would allow us to build the process of reflecting upon the failed proof in order to find an error into our automated proof tools making them more attractive to actual programmers.

My work focuses on functional programs produced by novice programmers. Functional programs are good subjects for the application of proof techniques and so provide a firm foundation for testing my hypothesis about the relation between programmer errors and proof failure. It is also relatively easy to obtain a large corpus of novice programs many of which contain errors.

People

• Louise Dennis
• Raul Monroy
• Pablo Nogueria-Iglesias

Funding

• EPSRC grant GR/S01771/01: The Integration and Interaction of Multiple Mathematical Reasoning Processes
• Nottingham NLF grant 3051: Classifying Programming Errors and how they Cause Correctness Proofs to Fail

Publications

• L. A. Dennis, Enhancing Theorem Prover Interfaces with Program Slice Information. User Interaces for Theorem Provers 2006, Seattle, Washington, 2006. Workshop associated with IJCAR 2006. Published in Electronic Notes in Computer Science, Volume 174, Issue 2, 2007.
• L. A. Dennis, Program Slicing and Middle-Out Reasoning for Error Location and Repair. IJCAR 2006 workshop on Disproving: Non-Theorems, Non-Validity and Non-Provability, Seattle, Washington, 2006.
• L. A. Dennis, R. Monroy and P. Nogueira. Proof-directed Debugging and Repair in H. Nilsson and M. van Eekelen (eds). Seventh Symposium on Trends in Functional Programming, pp. 131-140. 2006.
• L. A. Dennis Using Proof to Reason about Errors in Ontology Construction, Edinburgh Dream Group Blue Book Note 1536.
• L. A. Dennis and P. Nogueira. What can be Learned from Failed Proofs of Non-Theorems? in J. Hurd, E. Smith and A. Darbari (eds). Theorem Proving in Higher Order Logics (TPHOLs 2005): Emerging Trends Proceedings, pp. 45-58. Technical Report PRG-RP-05-2, Oxford University Computer Laboratory, 2005.
• L. A. Dennis, The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs, in W. Ahrendt and P. Baumgartner and H. de Nivelle (Eds): IJCAR 2004 Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability. pp. 47-58. 2004.
• Louise Dennis & Raul Monroy, Fault Diagnosis, Edinburgh Dream Group Blue Book Note 1485.
• Louise Dennis, Generating Counter-Examples from Corrective Predicates, Edinburgh Dream Group Blue Book Note 1490.

Code and Theories

Lambda-Clam Theories used for the work described in the IJCAR 2004 Paper

• basecases.mod, basecases.sig

Links

• Isabelle Home Page
• Lambda-Clam Home Page
• Grand Challenge 6: Dependable Systems Evolution

Bibliography

Bundy, 91

A. Bundy, A Science of Reasoning, in J.-L. Lassez and G. Plotkin (eds), Computational Logic: Essays in Honor of Alan Robinson, pp. 178-198, MIT Press, 1991.

Gordon and Melham, 93

M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.

Morris and Jones, 84

F. L. Morris and C. B. Jones. An Early Program Proof by Alan Turing. Annals of the History of Computing, 6:139-143, 1984.

Naur, 66

P. Naur. Proof of algorithms by general snapshots. BIT, 6:310-316, 1966. Mathematical Proofs

Paulson, 94

L. C. Paulson. Isabelle: a Generic Theorem Prover. Springer-Verlag Berlin and Heidelberg GmbH & Co. 1994.

Paulson, 98

L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols, Journal of Computer Security, 6:85-128, 1998.