## Refinement and the Z Schema Calculus

**CS-TR-02-31**
**Authors:** Lindsay Groves

**Source:** GZipped PostScript *(218kb)*

Adobe PDF
*(279kb)*

It is well known that the principal operators in the Z schema calculus are not
monotonic with respect to refinement, which limits their usefulness in software
development. The usual reaction to this observation is to remove all schema
operators before performing any kind of refinement, or to move to a different
formalism such as B or the refinement calculus. This paper examines the
interaction between refinement and the schema calculus more closely, showing
exactly how non-monotonicity arises, and identifying various conditions under
which components of schema expressions can be safely replaced by their
refinements. This analysis uses an alternative characterisation of refinement,
and a decomposition of the standard refinement relation into two simpler
relations that allow us to study refinements that modify a specification in
different ways.

[Up to Computer Science Technical Report Archive: Home Page]