The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs
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 th...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
2004
|
| Online Access: | https://eprints.nottingham.ac.uk/318/ |
| _version_ | 1848790391578427392 |
|---|---|
| author | Dennis, Louise Abigail |
| author2 | Ahrendt, W |
| author_facet | Ahrendt, W Dennis, Louise Abigail |
| author_sort | Dennis, Louise Abigail |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:11:52Z |
| format | Conference or Workshop Item |
| id | nottingham-318 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:52Z |
| publishDate | 2004 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3182020-05-04T20:31:25Z https://eprints.nottingham.ac.uk/318/ The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs Dennis, Louise Abigail 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. Ahrendt, W Baumgartner, Peter de Nivelle, H 2004 Conference or Workshop Item PeerReviewed Dennis, Louise Abigail (2004) The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs. In: IJCAR 2004 Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability, July 2004, Cork, Ireland. |
| spellingShingle | Dennis, Louise Abigail The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs |
| title | The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs |
| title_full | The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs |
| title_fullStr | The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs |
| title_full_unstemmed | The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs |
| title_short | The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs |
| title_sort | use of proof planning critics to diagnose errors in the base cases of recursive programs |
| url | https://eprints.nottingham.ac.uk/318/ |