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].
KeywordsProof Obligation Body Specification Strong Degree Internal Detail Predicate Part
Unable to display preview. Download preview PDF.