Abstract
Our insight into developing loops comes from the Invariance Theorem:
where P is a predicate called a loop invariant, and t is an integer function called the bound function. Conjunct (a) is the requirement of Invariance, conjunct (b) is the requirement of Progress, and conjunct (c) is the requirement of Boundedness.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1990 Springer-Verlag New York Inc.
About this chapter
Cite this chapter
Cohen, E. (1990). Developing loops — an introduction. In: Programming in the 1990s. Texts and Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4613-9706-9_9
Download citation
DOI: https://doi.org/10.1007/978-1-4613-9706-9_9
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-97382-1
Online ISBN: 978-1-4613-9706-9
eBook Packages: Springer Book Archive