A logical framework for software proof reuse

ABSTRACT

We describe a logical framework PR for verification of reusable software components. Within our system, developers can employ the advantages traditionally associated with software reuse to reduce the cost of software verification by reusing abstract proofs and specifications. One can construct an algorithm with parameters, a specification with parameters, and a proof that the algorithm satisfies the specification provided the parameters satisfy certain conditions. Proofs in PRwill themselves contain parameters for subproofs concerning those conditions. In this framework, typing, type checking, and proof checking are decidable.

REFERENCES

• 1: Arnon Avron , Furio Honsell , Ian A. Mason , Robert Pollack, Using typed lambda calculus to implement formal systems on a machine, Journal of Automated Reasoning, v.9 n.3, p.309-354, Dec. 1992 [doi>10.1007/BF00245294]
• 2: J. E. CAPLAN, Formalizing Hoare Logic, in Second ACM SIGPLAN Workshop on State in Programming Languages, San Francisco, Jan. 1995, Association for Computing Machinery, pp. 1-18. Available as University of Illinois at Urbana-Champaign tech. reg. UIUCDCS-R-95-1900.
• 3: R. L. CONSTABLE AND S. F. SMITH, Partial objects in constructive type theory, in Symposium on Logic in Computer Science, Ithaca, New York, 1987, pp. 183- 193.
• 4: M. J. C. GORDON, R. MILNEa, AND C. P. WADS- WORTH, Edinburgh LCF : a mechanised logic of computation, vol. 78 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1979.
• 5: M. T. HARANDI AND F. H. YOUNG, Software design using reusable algorithm abstractions, in Software Engineering 88, University of Liverpool, July 1988, Institution of Electrical Engineers/British Computer Society, The Institution, pp. 93-97.
• 6: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 7: I. A. MASON, Hoare's Logic in the LF, Tech. Rep. ECS-LFCS-87-32, Laboratory for the Foundations of Computer Science, Edinburgh, Scotland, 1987.
• 8: Bengt Nordström , Kent Petersson , Jan M. Smith, Programming in Martin-Lo¨f's type theory: an introduction, Clarendon Press, New York, NY, 1990
• 9: P. W. O'HEARN AND R. D. TENNENT, Syntactic control o/interference revisited, May 1994.
• 10: John C. Reynolds, Syntactic control of interference, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.39-46, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512766]
• 11: ~, The essence o} ALGOL, in Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, eds., North-Holland, 1981, pp. 345-372.
• 12: ~, Idealized ALGOL and its specification logic, in Tools and Notions for Program Construction: An Advanced Course, D. N~el, ed., Cambridge University Press, 1982, pp. 121-161.
• 13: John C. Reynolds, Syntactic Control of Inference, Part 2, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.704-722, July 11-15, 1989
• 14: S. F. Smith, Partial objects in type theory, Cornell University, Ithaca, NY, 1989
• 15: ~, Partial computations in constructive type theory, tech. rep., The Johns Hopkins University, Baltimore, Maryland, Feb. 1991.
• 16: V. SwAmrP, Type Theoretic Properties of Assignments, PhD thesis, University of Illinois at Urbana- Champaign, Urbana, Illinois, 1992.
• 17: Simon Thompson, Type theory and functional programming, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1991

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.m Miscellaneous
          Subjects: Reusable software**

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Theory