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

Unknown, Conference object English OPEN
Dennis, Louise Abigail (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 Lambda-clam, a proof planning system, and applied successfully to a small set of examples.
  • References (18)
    18 references, page 1 of 2

    [1] A. Bundy. A science of reasoning. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 178{198. MIT Press, 1991.

    [2] A. Bundy. The automation of proof by mathematical induction. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1. Elsevier, 2001.

    [3] A. Bundy, F. van Harmelan, C. Horn, and A. Smaill. The oyster-clam system. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Arti cial Intelligence, pages 647{648. Springer, 1990.

    [4] H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + rst-order consistency. Information and Computation, 159(1{2), 2000.

    [5] L. A. Dennis and J. Brotherston. clam v4: User/Developer's Manual. Mathematical Reasoning Group, Division of Informatics, University of Edinburgh, 2002.

    [6] L. Dixon and J. D. Fleuriot. IsaPlanner: A prototype proof planner in Isabelle. In F. Baader, editor, 19th International Conference on Automated Deduction, volume 2741 of Lecture Notes in Computer Science, pages 279{283. Springer, 2003.

    [7] M. Franova and Y. Kodrato . Predicate synthesis from formal speci cation. In B. Neumann, editor, 10th European Conference on Arti cial Intelligence, pages 97{91. John Wiley and Sons, 1992.

    [8] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

    [9] J. Gow. The Dynamic Creation of Induction Rules Using Proof Planning. PhD thesis, Centre for Intelligent Systems and their Applications, School of Informatics, University of Edinburgh, 2004.

    [10] A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1{2):79{111, 1996.

  • Metrics
    No metrics available
Share - Bookmark