This paper presents a method of reasoning about Object-Z specifications. The approach utilizes the modularity inherent in Object-Z specifications to simplify proofs. Properties proved for a class in isolation can be used when that class is either inherited by another class or instantiated as part of a system of interacting objects. Proofs using structural induction and the notion of object integrity are discussed.
Index Terms:
Object-Z, formal reasoning, proof systems, object orientation
Citation:
Graeme Smith, "Reasoning about Object-Z Specifications," apsec, pp.489, Second Asia-Pacific Software Engineering Conference (APSEC'95), 1995