Browse Prior Art Database

Original Publication Date: 1973-May-01
Included in the Prior Art Database: 2005-Sep-20

Publishing Venue

Software Patent Institute

Related People

Deutsch, L.P.: AUTHOR [+2]


This thesis is about automatic program verification. Program verification refers to the idea that one can state the intended effect of a program in a precise way that is not merely another program, and then prove rigorously that the program does (or does not) conform to this specification. Automatic refers to the hope that if we can understand enough about the structure of programs and the structure of proofs, we can build systems that perform some or all of this verification task for us. The computing community has two good reasons for being interested in automatic verification. The first is practical. Most large software systems never work reliably, and a study suggests ( Belady, L. A., and Lehman, M. M., Programming System Dynamics, or, The Meta-Dynamics of Systems in Maintenance and Growth, report RC 3546, IBM T. J. Watson Research Center, Yorktown Heights, N. J., Sept. 1971) that the initial quality of such systems has a surprisingly large influence over their reliability during their entire lifetime. For such systems, it is clear that automated aids to verification will be required, since hand-verification would be impossibly tedious. In the short run, the ";structured programming"; approach of Dijkstra ( Dijkstra, E. W., Structured Programming Software Engineering Techniques, J. N. Buxton and B. Randall (eds.) Oct. 1969, pp. 84 - 88) , which attempts to codify and enforce good programming practices such as limiting interactions between program modules, is likely to prove more valuable than verification: this approach is already being adopted ( Mills, H. D., Structured Programming in Large Systems, Debugging Techniques in Large Systems, R. Rustin (ed.), Prentice Hall Inc., Englewood Cliffs, N. J., pp. 41 - 55) in an effort to hold down software costs. However, such an approach can only reduce the likelihood of errors, and does not offer the kind of security attainable through verification. Another idea advocated by a few, that of ";graceful recovery"; from software errors ( Baskin, H. B., Borgerson, B. R., Roberts, R., PRIME - A modular architecture for terminal-oriented systems, Proceedings of the 1972 SJCC, AFIPS Press, N. J., pp. 431 - 437) , seems like a serious misapplication of an idea which works very well for hardware errors. Verification is also important to computing because of its place in the historical trend which has constantly brought programming languages closer to the problem domain of the end user. This process has required transferring more and more of what were originally thought of as ";programming"; tasks to the machine, and this in turn has required increasingly deep understanding of the process of programming. The author believes that his automatic verification system succeeds as well as it does because it represents a successful encoding of the structure of programs. To this extent, it constitutes a contribution to the emerging area of automatic programming, a term which refers to a group of ambitious attempts to throw much more of the detailed design of algorithms and data structures onto the machine than was previously thought possible. A recent survey by Balzer ( Balzer, R. M., Automatic Programming, Institute Technical Memorandum, University of Southern California, Information Sciences Institute, Sept. 1972, (rough draft)) gives a good idea of the scope of these attempts. The author has built and checked out an automatic verification system called PIVOT (Programmer's Interactive Verification and Organizational Tool). There has been one other published automatic verification system, that of James C. King, reported in his Ph.D. thesis (issued in 1970). PIVOT owes an enormous amount to King's system in certain specific areas, notably representation and simplification of arithmetic expressions, although the organization of PIVOT is quite different from that of King's Verifier. There will be numerous references and comparisons to King's work strewn throughout this thesis. However, there have been considerable advances in artificial intelligence in the past three years, and the present work has made use of some of them, particularly the work of the QA4 group at Stanford Research Institute (Derksen, Rulifson, Waldinger, et al.) ( Rulifson, J. F., Derksen, J. A., and Waldinger, R. J., QA4: A Procedure Calculus for Intuitive Reasoning, Stanford Research Institute Technical Report, Nov. 1972) to which there will also be frequent references. Perhaps the most interesting result of the author's experiences over the year and a half spent developing PIVOT is the observation that program verification seems to be a task significantly different from that of proving mathematically interesting theorems. The verification task involves verifying the consistency of a network of state descriptions: the verification of each individual arc of this network, which corresponds to a partial path through the program, is as much like executing the program in an abstract algebraic domain as it is like proving theorems about what the program is doing. This observation has been made independently by other researchers [ Footnote ] [ endnotes ] Burstall, R. M., and Topor, R., Mechanizing Program Correctness Proofs by Symbolic Interpretation, (note on work in progress -- privately circulated), Nov. 1972. Robinson, J. A., (private communication) . The author was not committed to this view when he began; it arose progressively from his experience with his system. The sections ";Program overview"; and ";Theorem generator"; in the next chapter will describe the structure of the system in more detail in this regard.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 3% of the total text.

Page 1 of 66


©; Xerox Palo Alto Research Center, May, 1973



Program verification refers to the idea that the intent or effect of a program can be stated in a precise way that is not a simple "rewording" of the program itself, and that one can prove (in the mathematical sense) that a program actually conforms to a given statement of intent. This thesis describes a software system which can verify (prove) some non-trivial programs automatically.

The system described here is organized in a novel manner compared to most other theorem- proving systems. It has a great deal of specific knowledge about integers and arrays of integers, yet it is not "special-purpose", since this knowledge is represented in procedures which are separate from the underlying structure of the system. It also incorporates some knowledge, gained by the author from both experiment and introspection, about how programs are often constructed, and uses this knowledge to guide the proof process. It uses its knowledge, plus contextual information from the program being verified, to simplify the theorems dramatically as they are being constructed, rather than relying on a super-powerful proof procedure. The system also provides for interactive editing of programs and assertions, and for detailed human control of the proof process when the system cannot produce a proof (or counter-example) on its own.

KEY WORDS program verification, theorem proving, interactive systems, context trees

4.19, 4.22, 5.21, 5.24



Chapter I: Preliminaries Introduction.....I-4
Theoretical Background.....I-5
Chapter II: Input Language

Program Structure.....II-1
Chapter III: Processing Structure

Program Overview.....III-1
Theorem Generator.....III-8
Theorem Prover.....III-12
Chapter IV: Deduction

Xerox Corporation Page 1 May 01, 1973

Page 2 of 66


     Data Base Overview.....IV-1
Value Data Bases.....IV-2
Clause Data Bases.....IV-6
Chapter V: Representation and Simplification

     Expression Overview.....V-1
Arithmetic Expressions.....V-3
Logical Expressions.....V-5
Source Program.....V-13
Chapter VI: Human Interface

     Editing Language.....VI-1
Executive Language.....VI-3
Proof Control Language.....VI-7
Incremental Aspects.....VI-9
Chapter VII: Conclusions

     Accomplishments and Failures.....VII-1
Soundness and Completeness.....VII-2
Comments and Prospects.....VII-4
Appendix A: Example with key to trace output Appendix B: Automatic proof of Constable-Gries program Appendix C: Analysis of Floyd's "Interactive Design" scenario Appendix D: Programs successfully verified

[ chapter 1 ] Preliminaries