Interactive proof checking

ABSTRACT

Knowledge of logical inference rules allows a specialized proof editor to provide a user with feedback about errors in a proof under development. Providing such feedback involves checking a collection of constraints on the strings of the proof language. Because attribute grammars allow such constraints to be expressed in a modular, declarative fashion, they are a suitable underlying formalism for a proof-checking editor. This paper discusses how an attribute grammar can be used in an editor for partial-correctness program proofs in Hoare-style logic, where verification conditions are proved using the sequent calculus.

REFERENCES

• 1: Joseph L. Bates , Robert L. Constable, Proofs as Programs, Cornell University, Ithaca, NY, 1983
• 2: Bricklin, D. and Frankston, B. VisiCale Computer Software Program for the Apple II and II Plus. Personal Software, Inc., Sunnyvale, Calif., 1979.
• 3: R. L. Constable , S. D. Johnson , C. D. Eichenlaub, An Introduction to the PL/CV2 Programming Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 4: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 5: Feldman, S.I. Make—A program for maintaining computer programs. Software—Practice, and Experience 9, 4 (April 1979), 255-265.
• 6: Gentsen, G. Investigations into logical deductions. In The Collected Papers of Gerhard Gentsen, M.E. Szabo (ed.), North-Holland, Amsterdam, 1969, pp. 68-131.
• 7: Susan L. Gerhart, Correctness-preserving program transformations, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.54-66, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512983]
• 8: Gordon, M., Milner, R., and Wadsworth, C. Lecture Notes in Computer Science, vol. 78: Edinburgh LCF. Springer-Verlag, New York, 1979.
• 9: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 10: Scott D. Johnson, A Computer System for Checking Proofs, Cornell University, Ithaca, NY, 1981
• 11: Kleene, S.C. Introduction to Metamathematics. North-Holland, Amsterdam, 1952.
• 12: Knuth, D.E. Semantics of context-free languages. Math. Syst. Theory 2, 2 (June 1968), 127-145.
• 13: Dean B. Krafft, AVID: A system for the Interactive Development of Verifiably Correct Programs, Cornell University, Ithaca, NY, 1981
• 14: D. R. Milton , L. W. Kirchhoff , B. R. Rowland, An all(1) compiler generator, Proceedings of the 1979 SIGPLAN symposium on Compiler construction, p.152-157, August 06-10, 1979, Denver, Colorado, United States
• 15: Moriconi, M. A designer/verifier's assistant. IEEE Trans. Softw. Eng. SE-5, 4 (July 1979), 387-401.
• 16: Nelson, G. Techniques for program verification. Tech. Rep. CSL-81-10, Xerox Palo Alto Research Center, Palo Alto, Calif., June 1981.
• 17: Thomas W. Reps, Generating language-based environments, Massachusetts Institute of Technology, Cambridge, MA, 1984
• 18: Reps, T., and Teitelbaum, T. The Synthesiser Generator. Dept. of Computer Science, Cornell Univ., Ithaca, N.Y., Oct. 1983.
• 19: Thomas Reps , Tim Teitelbaum , Alan Demers, Incremental Context-Dependent Analysis for Language-Based Editors, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.449-477, July 1983 [doi>10.1145/2166.357218]
• 20: Bruce Ramon Rowland, Combining parsing and evaluation for attributed grammars., 1977
• 21: Turing, A.M. On computable numbers with an application to the Entscheidungsproblem. Proc. London Math. Soc., ser. 2, 42(1936-7), 230-265.
• 22: Watt, D.A. The parsing problem for affix grammars. Acta Informatica 8(1977), 1-20.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Design, Performance, Verification