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 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.

A Comparison of two Proof Critics: Power vs. Robustness

Proof critics are a technology from the proof planning paradigm. They examine failed proof attempts in order to extract information which can be used to generate a patch which will allow the proof to go through. We consider the proof of the $quot;whisky problem$quot;, a challenge problem from the domain of temporal logic. The proof requires a generalisation of the original conjecture and we examine two proof critics which can be used to create this generalisation. Using these critics we believe we have produced the first automatic proofs of this challenge problem. We use this example to motivate a comparison of the two critics and propose that there is a place for specialist critics as well as powerful general critics. In particular we advocate the development of critics that do not use meta-variables.

'Dis ain't gimme, Florida': Zora Neale Hurston's Their Eyes Were Watching God

Who owns Zora Neale Hurston? That was the question asked in 1990 by Michele Wallace, in an analysis of the ways in which Hurston has been appropriated by later scholars. Wallace's pungent comparison of later critics to so many 'groupies descending on Elvis Presley's estate' in their haste to turn Hurston to their own purposes strikes a cautionary note for any subsequent writer. As she notes, the risk of canonization is that the work will be misused to derail the future of blackwomen in literature and literary criticism. For Wallace, Harold's introduction to his Modern Critical Views anthology of 1986 is a case in point. This article is copyright 2003 MHRA, and is included in this repository with permission.