Reasoning about Object-Z specifications
Graeme Smith · 2002
This paper presents a method of reasoning about Object-Z specifications. The approach utilises 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.