Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

In this paper we present a new and practical approach to program verification based on the transformational program development method. We believe this system, which we call the Practical Verification System, is both user-friendly and mathematically powerful. A user of this system would present the system with an initial abstract specification, written in the user-interface language, and the system, under the guidance of the user, would generate a program guaranteed to satisfy the goals set forth in the initial specification. The advantages of the transformational method are its potential ability to act as a rich source of high-level, reusable theorems, to allow efficient verification of resulting programs, and to track the user's understanding of a program. Simplicity of design is also achieved through the use of a single, powerful internal language, and through reliance on a large information database.

REFERENCES

• 1: P. R. Eggert, Overview of the Ina Jo Specification Language, System Development Corporation TM(L)-6021/001/00, Santa Monica, CA, 1980.
• 2: K. Levitt, The HDM Handbook, Vol. 1, SRI International, Menlo Park, CA 94025, 1979.
• 3: S. L. Gerhart, AFFIRM User's Guide, USC Information Sciences Institute, Marina del Rey, California, 1979.
• 4: D. Good, et al, Report on the Language Gypsy, ISCA-CMP-10, September 1978.
• 5: F. L. Bauer, "Programming as an Evolutionary Process," Language Hierarchies and Interfaces, Lecture Notes in Computer Science, Vol. 46, Springer-Verlag, New York, 1976.
• 6: M. Broy, P. Pepper, "Program Development as a Formal Activity," IEEE Trans. Software Eng., Vol. SE-7, January 1981.
• 7: D. S. Wile, "Type Transformations," IEEE Trans. Software Eng., Vol. SE-7, January 1981.
• 8: P. London and M. Feather, "Implementing Specification Freedoms", Science of Computer Programming 2, North Holland Publishing Company, 1982, pp. 91-131.
• 9: D. S. Wile, "POPART: Producer of Parsers and Related Tools, System Builders Manual," Information Sciences Institute, October 1981.
• 10: J. G. Williams, "A logic for Reasoning About Programs", 3 MTP 240, The MITRE Corporation, January, 1984.
• 11: R. Boyer, and J. Moore, "The Mechanical Verification of a Fortran Square Root Program," SRI International, January, 1981.
• 12: Ewing L. Lusk , William McCune , Ross A. Overbeek, Logic Machine Architecture: Kernel Funtions, Proceedings of the 6th Conference on Automated Deduction, p.70-84, June 07-09, 1982
• 13: Valdis Andris Berzins, Abstract model specifications for data abstractions, 1979
• 14: L. Flon and J. Misra, "A Unified Approach to the Specification and Verification of Abstract Data Types," Proceedings of the IEEE Conference on Specifications of Reliable Software, Cambridge, Massachusetts, April, 1979.
• 15: Alfred V. Aho , Jeffrey D. Ullman, Principles of Compiler Design (Addison-Wesley series in computer science and information processing), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1977
• 16: Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 17: L. F. Rubin, "Syntax-Directed Pretty Printing - A First Step Towards a Syntax-Directed Editor," IEEE Transactions on Software Engineering, Vol. SE-9, No. 2, March 1983.
• 18: H. Leblanc, and W. A. Wisdom, Deductive Logic, Second Edition, Allan and Bacon, Boston, 1976.
• 19: Patrick Henry Winston, Artificial intelligence (2nd ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1984
• 20: R. Boyer, and J. Moore, A Computational Logic, Academic Press Inc., 1979.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Verification