Monotonicity in Calculational Proofs - Correct System Design: Recent Insights and Advances - page 83

77, monotonicity of -body is used without mention. We think the authors just

didn't anticipate the frequent use of monotonicity and the problem readers would
have with it if it were not well explained.
Gries and Schneider [3] also don't treat montonicity well, and this has resulted
in confusion among students about monotonicity and its use. The next edition
of [3] is expected to use the approach of this note in order to eliminate the
confusion.
The message of this little article is meant to be the apparent simplicity and
brevity of many proofs in the calculational system when the right tools, like
metatheorem Monotonicity, are available.

8

Acknowledgements

Thanks to an anonymous referee, who helped improve this presentation.

References

1. Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Se-
mantics . Springer Verlag, New York, 1990.
2. Wim H.J. Feijen. 98 ) 89 . WHJ189, September 1994.
3. David Gries and Fred B. Schneider. A Logical Approach to Discrete Math .
Springer Verlag, New York 1993.
4. Carroll Morgan. Email communications in September 1995.