Logical analysis of programs
- 1 April 1976
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 19 (4) , 188-206
- https://doi.org/10.1145/360032.360048
Abstract
Most present systems for verification of computer programs are incomplete in that intermediate inductive assertions must be provided manually by the user, termination is not proven, and incorrect programs are not treated. As a unified solution to these problems, this paper suggests conducting a logical analysis of programs by using invariants which express what is actually occurring in the program.The first part of the paper is devoted to techniques for the automatic generation of invariants. The second part provides criteria for using the invariants to check simultaneously for correctness (including termination) or incorrectness. A third part examines the implications of the approach for the automatic diagnosis and correction of logical errors.Keywords
This publication has 9 references indexed in Scilit:
- Finding Invariant assertions for proving programsPublished by Association for Computing Machinery (ACM) ,1975
- Towards automatic debugging of programsPublished by Association for Computing Machinery (ACM) ,1975
- The synthesis of loop predicatesCommunications of the ACM, 1974
- Reasoning about programsArtificial Intelligence, 1974
- Proof of a programCommunications of the ACM, 1971
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- The correctness of programsJournal of Computer and System Sciences, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967
- A Class of Non-Analytical Iterative ProcessesThe Computer Journal, 1959