Louise Abigail Dennis
The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs
Dennis, Louise Abigail
Authors
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
basecases.pdf
(122 Kb)
PDF
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search