Skip to main content

Research Repository

Advanced Search

The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs

Dennis, Louise Abigail

The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs Thumbnail


Authors

Louise Abigail Dennis



Contributors

W Ahrendt
Editor

Peter Baumgartner
Editor

H de Nivelle
Editor

Abstract

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 Lambda-clam, a proof planning system, and applied successfully to a small set of examples.

Citation

Dennis, L. A. The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs. Presented at IJCAR 2004 Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability

Conference Name IJCAR 2004 Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability
Publication Date Jan 1, 2004
Deposit Date Nov 22, 2005
Publicly Available Date Oct 9, 2007
Peer Reviewed Peer Reviewed
Public URL https://nottingham-repository.worktribe.com/output/1021365

Files





Downloadable Citations