Z Expression of Refinable Objects
This chapter describes an approach to specifying objects in Z which is particularly appropriate if the specifications are to be used for subsequent refinement and proof. When carrying out such proof it is useful to be able to provide a strong degree of separation between the objects so that it is possible to reason about the use of those objects without having to consider their internal details. The particular approach described here is motivated in some detail in [Whysall and McDermid 1991a] and [Whysall and McDermid 1991b].
Unable to display preview. Download preview PDF.