Modular reasoning in Object-Z

One of the tasks of a formal specification validation activity is to prove that systems described by the specification exhibit certain properties. For specifications describing large and complex systems, this can be difficult. Modular reasoning is an approach to this task in which one views a system as a number of smaller; simpler components, and where one attempts to carry out most of the reasoning at the component level. The paper describes a framework for conducting modular reasoning about Object-Z specifications. Using the strictly modular semantics of Object-Z as a foundation, the author formalises the notions of object property and system property. She presents results that enable object properties, which are the product of modular reasoning, to be used in the proof of system properties. The ideas are illustrated via the specification and partial validation of a small example