The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs
Louise A. Dennis · Nottingham ePrints (University of Nottingham) · 2004
This paper reports the use of proof planning to diagnose errors in program code. In particular it looks at the errors that arise in the base cases of recursive programs produced by undergraduates. It describes two classes of error that arise in this situation. The use of test cases would catch these errors but would fail to distinguish between them. The system adapts proof critics, commonly used to patch faulty proofs, to diagnose such errors and distinguish between the two classes. It has been implemented in λClam, a proof planning system, and applied successfully to a small set of examples. The use of mathematical proof to show that a computer program meets its specification has a long history in Computer Science (e.g. [14, 13]). Considerable time and effort has been invested in creating computer-based tools to support the process of proving programs correct (e.g. [15, 8]). However the technique and tools are only used in very specialised situations in industry where programmers generally rely on testing and bug reports from users to assess the extent to which a program meets its specification.