Issue No.01 - March (1975 vol.1)
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.
Generators, Humans, Educational institutions, Knowledge based systems, Computers, Sorting, Interactive systems, theorem proving, Correctness, interactive system, program proving, program verification, reliable software, simplification
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