The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.01 - March (1975 vol.1)
pp: 59-67
W. W. Bledsoe , Department of Computer Sciences, University of Texas, Austin, Tex. 78712
ABSTRACT
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
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
16 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool