Z Expression of Refinable Objects

  • Peter J. Whysall
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


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].


Proof Obligation Body Specification Strong Degree Internal Detail Predicate Part 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 1992

Authors and Affiliations

  • Peter J. Whysall
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkHeslington, YorkUK

Personalised recommendations