@article{bd9f3f51ed7e443b8a5309b5445770f7,
title = "Derivation of Invariant Assertions During Program Development by Transformation",
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 = "assertions, invariants, iteration, program development, program transformations, recursion, recursion removal, specification, verification",
author = "Manfred Broy and Bernd Krieg-Bruckner",
note = "Funding Information: Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission. This research was supported in part by the Sonderforschungsbereich 49-Programmiertechnik ({"} Software Engineering{"}), Munich, Germany, and in part by the National Science Foundation under Gran t MCS74-07644-A04. Authors' present addresses: M. Broy, Institut fiir Informatik, Technische Universit\textasciitilde{}t Miinchen, Postfach 202420, 8000 Mtinchen 2, West Germany; B. Krieg-Brdckner, Computer Science Division--EECS, University of California at Berkeley, Berkeley, CA 94720. {\textcopyright} 1980 ACM 0164-0925/80/0700-0321 \$00.75 ACM Transactions on Programming Languages and Systems, Vol. 2, No. 3, July 1980, Pages 321-337.",
year = "1980",
month = jul,
day = "1",
doi = "10.1145/357103.357108",
language = "English",
volume = "2",
pages = "321--337",
journal = "ACM Transactions on Programming Languages and Systems (TOPLAS)",
issn = "0164-0925",
publisher = "Association for Computing Machinery (ACM)",
number = "3",
}