This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An interactive program verification system
March 1975 (vol. 1 no. 1)
pp. 59-67
Donald I. Good, Department of Computer Sciences, University of Texas, Austin, Tex. 78712
Ralph L. London, University of Southern California Information Sciences Institute, Marina del Rey, Calif
W. W. Bledsoe, Department of Computer Sciences, University of Texas, Austin, Tex. 78712
This paper is an initial progress report on the development of an interactive system for verifying that computer programs meet given formal specifications. The system is based on the conventional inductive assertion method: given a program and its specifications, the object is to generate the verification conditions, simplify them, and prove what remains. The important feature of the system is that the human user has the opportunity and obligation to help actively in the simplifying and proving. The user, for example, is the primary source of problem domain facts and properties needed in the proofs. A general description is given of the overall design philosophy, structure, and functional components of the system, and a simple sorting program is used to illustrate both the behavior of major system components and the type of user interaction the system provides.
Index Terms:
Generators,Humans,Educational institutions,Knowledge based systems,Computers,Sorting,Interactive systems,theorem proving,Correctness,interactive system,program proving,program verification,reliable software,simplification
Citation:
Donald I. Good, Ralph L. London, W. W. Bledsoe, "An interactive program verification system," IEEE Transactions on Software Engineering, vol. 1, no. 1, pp. 59-67, March 1975, doi:10.1109/TSE.1975.6312820
Usage of this product signifies your acceptance of the Terms of Use.