Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

A SURVEY OF PROGRAM PROOF TECHNOLOGY

IP.com Disclosure Number: IPCOM000128228D
Original Publication Date: 1978-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 20 page(s) / 72K

Publishing Venue

Software Patent Institute

Related People

Jacob T. Schwartz: AUTHOR [+3]

Abstract

The problem of proving programs correct has existed since the first computers were constructed, and has steadily grown more pressing as programs have increased in complexity. The large number of papers (close to 800) that have been written in this-area have established program verification as a recognised subfield of computer science. But in spite of all this work, a truly practical program verification technology has been slow to develop, and is still not at hand. Indeed, the history to date of program. verification makes one key fact quite clear: The problem of verifying large programs rigorously is a very difficult one, and its solution will imply significant changes in current programming technology. This paper will review various salient aspects of the verification problem, assess progress to date, point out major difficulties which remain, and attempt to project future directions of progress.

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

Page 1 of 20

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

A SURVEY OF PROGRAM PROOF TECHNOLOGY

BY Jacob T. Schwartz September 1978

Report No. 001 "This material is based upon work supported by the Office of Naval Research under Contract Tao. N00014-78-C-Ou39, (P1R043-430)." The problem of proving programs correct has existed since the first computers were constructed, and has steadily grown more pressing as programs have increased in complexity. The large number of papers (close to 800) that have been written in this-area have established program verification as a recognised subfield of computer science. But in spite of all this work, a truly practical program verification technology has been slow to develop, and is still not at hand. Indeed, the history to date of program. verification makes one key fact quite clear: The problem of verifying large programs rigorously is a very difficult one, and its solution will imply significant changes in current programming technology. This paper will review various salient aspects of the verification problem, assess progress to date, point out major difficulties which remain, and attempt to project future directions of progress.

2. How is it possible to -prove programs corrects?

To prove programs correct, one can begin by giving formal mathematical defiai.tion to the notions- 'program' and 'progr= execation'. Essentially, these mathematical definitions merely formalise the basic facts concerning programs and their meaning that one would present in a first course on programming. A 'program' can be defined formally as a sequence of 'statements'., where each statement is a syntactic structure of one of the three forms

variable := expression; or if expression then substatementl else substatement2; or while expression do substatement;

(Of course, depending ow the richness of the prograamni.ng language Z with which one is working, a few other farms of statement may also have to be considered.) The 'state' of a program is a mapping which defines the current value of every variable appearing in the program, and which also defines a 'current control location', i.e., the particular statement of the program which is to be executed next. Execution of a. statement changes this state according to familiar, well defined rR.iles (these are just the rules that have to be explained in an elementary programming course to students meeting the programming language L for the first time; we can call them the

'transition rules' of L ). The 'state sequence' corresponding to a program P is the sequence of states whose first state is defined by the initialisation rules of the language L , and in which each subsequent state is obtained from the state which preceeds it by application of the appropriate transition rule of L . Thus the state sequence of the program P is uniquely defined by the text of P . To prove P correct is to prove some desired property of this state sequence rigorously. Although direct, elemen...