The schema calculus of Z provides a means for expressing structured, modular specifications. Extending this modularity to program development requires the monotonicity of these operators with respect to refinement. This paper provides a thorough mathematical analysis of monotonicity with respect to four schema operations for three notions of operation refinement. The mathematical connection between the equational schema logic and monotonicity is discussed and evaluated.
展开▼
