Browse Prior Art Database

AN INTERACTIVE PROGRAM VERIFIER

IP.com Disclosure Number: IPCOM000128895D
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 [+3]

Abstract

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.

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

Page 1 of 66

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

©; Xerox Palo Alto Research Center, May, 1973

AN INTERACTIVE PROGRAM VERIFIER

BY L. PETER DEUTSCH CSL-73-1 MAY 1973 REPRINTED JULY 1976

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

CR CATEGORIES
4.19, 4.22, 5.21, 5.24

XEROX PALO ALTO RESEARCH CENTER 3333 COYOTE HILL ROAD/PALO ALTO/CALIFORNIA 94304

TABLE OF CONTENTS

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

Program Structure.....II-1
Declarations.....II-5
Statements.....II-6
Expressions.....II-8
Chapter III: Processing Structure

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

Xerox Corporation Page 1 May 01, 1973

Page 2 of 66

AN INTERACTIVE PROGRAM VERIFIER

     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
Quantifiers.....V-8
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
Bibliography
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

Introduction...