Some Aspects of the Verification of Loop Computations
- 1 November 1978
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. SE-4 (6) , 478-486
- https://doi.org/10.1109/tse.1978.233871
Abstract
The problem of proving whether or not a loop computes a given function is investigated. We consider loops which have a certain "closure" property and derive necessary and sufficient conditions for such a loop to compute a given function. It is argued that closure is a fundamental concept in program proving. Extensions of the basic result to proofs involving relations other than functional relations, which typically arise in nondeterministic loops, are explored. Several applications of these results are given, particularly in showing that certain classes of programs may be directly proven (their loop invariants generated) given only their input-output relationships. Implications of these results are discussed.Keywords
This publication has 13 references indexed in Scilit:
- Logical analysis of programsCommunications of the ACM, 1976
- A view of program verificationACM SIGPLAN Notices, 1975
- Proving loop programsIEEE Transactions on Software Engineering, 1975
- An interactive program verification systemPublished by Association for Computing Machinery (ACM) ,1975
- Finding Invariant assertions for proving programsPublished by Association for Computing Machinery (ACM) ,1975
- The new math of computer programmingCommunications of the ACM, 1975
- Proving Theorems about LISP FunctionsJournal of the ACM, 1975
- A more mechanical approach to program verificationPublished by Springer Nature ,1974
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967