Abstract
In this paper an outline is given of an approach to formally reasoning about importation, parameterisation and instantiation of specifications written in a modular extension of the Z language (called Sum). Interpretation and instantiation of theories in first order logic are well understood. We illustrate how to use these results directly to provide a framework within which we can soundly and efficiently reason about modular specifications. A reasoning environment within the Ergo .1 theorem prover has been constructed that provides the theory management, construction and extension facilities needed to support such a reasoning process. Sum specification are mapped to the appropriate Ergo structures by a straightforward translation process. A simple case study in Sum is presented to demonstrate the use of these theory extension mechanisms. As far as the authors are aware, no other system offers automated support for reasoning about parameterisation and instantiation of modular model-oriented specifications.