A Comparative Analysis of Functional Correctness
- 1 June 1982
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Computing Surveys
- Vol. 14 (2) , 229-244
- https://doi.org/10.1145/356876.356881
Abstract
The functional correctness technique is presented and discussed. It is also explained that the underlying theory has an implicatmn for the derivation of loop invariants. The functional verification conditions concerning program loops are then shown to be a specialization of the commonly used inductive assertion verification conditions. Next, the functional technique is compared and contrasted with subgoal induction. Finally, the difficulty of proving initialized loop programs is examined in light of both the inductive assertion and functional correctness theories.Keywords
This publication has 10 references indexed in Scilit:
- A Comparison of the Axiomatic and Functional Models of Structured ProgrammingIEEE Transactions on Software Engineering, 1980
- Program correctness: on inductive assertion methodsIEEE Transactions on Software Engineering, 1980
- Some Aspects of the Verification of Loop ComputationsIEEE Transactions on Software Engineering, 1978
- Prospects and Limitations of Automatic Assertion Generation for Loop ProgramsSIAM Journal on Computing, 1977
- Complexity of Synthesizing Inductive AssertionsJournal of the ACM, 1977
- Subgoal inductionCommunications of the ACM, 1977
- The new math of computer programmingCommunications of the ACM, 1975
- Mathematical theory of partial correctnessJournal of Computer and System Sciences, 1971
- Formalization of Properties of Functional ProgramsJournal of the ACM, 1970
- An axiomatic basis for computer programmingCommunications of the ACM, 1969