Abstrac
In this chapter we show that the basic predicate transformers that we have introduced to model contracts (asserts, guards, functional updates, demonic and angelic updates) are all monotonic. In addition, composition, meet, and join preserve monotonicity. Conversely, any monotonic predicate transformer can be described in terms of these constructs, in a sense to be made more precise below. In fact, it is possible to write any monotonic predicate transformer in a normal form.
This is a preview of subscription content, log in via an institution to check access.
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
© 1998 Springer Science+Business Media New York
About this chapter
Cite this chapter
Back, RJ., von Wright, J. (1998). Statements. In: Refinement Calculus. Graduate Texts in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-1674-2_13
Download citation
DOI: https://doi.org/10.1007/978-1-4612-1674-2_13
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-98417-9
Online ISBN: 978-1-4612-1674-2
eBook Packages: Springer Book Archive