Derivation of Invariant Assertions During Program Development by Transformation
- 1 July 1980
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 2 (3) , 321-337
- https://doi.org/10.1145/357103.357108
Abstract
Two approaches to the development of efficient and correct iterative programs are contrasted: the construction of an iterative program and a proof of its correctness using invariant assertions of loops, and the construction and proof of a recursive program with a subsequent transformation into an iterative version by schematically applying suitable recursion removal rules. The connection between the approaches is demonstrated by augmenting such transformation rules by inductive assertions. It is argued that the latter approach to program development is superior since the correctness proof of a recursive program is easier in most cases. Considerable verification overhead can be avoided this way, in particular, some difficulties with the interaction of successive loops and their associated invariants.Keywords
This publication has 8 references indexed in Scilit:
- Subgoal inductionCommunications of the ACM, 1977
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977
- Logical analysis of programsCommunications of the ACM, 1976
- Primitive recursive program transformationPublished by Association for Computing Machinery (ACM) ,1976
- Translating recursion equations into flow chartsJournal of Computer and System Sciences, 1971
- Proof of a programCommunications of the ACM, 1971
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967