An Object-Oriented Structuring for Z Based on Views

There is significant interest in the use of Z in conjunction with object-orientation. Here we present a new approach to structuring Z specifications in an object-oriented (OO) style. Our structuring is based on views, it uses the schema calculus, and it does not extend Z. The resulting OO Z specifications are comprehensible, modular, and conceptually clear. The modularity of the new approach supports a templateinstantiation approach to expressing OO models in Z; practical formal verification and validation of the model can be undertaken using metaproof, meta-lemmas, and formal snapshots.

• Type: Conference
• Year: 2005
• Where: ZUM
• Authors: Nuno Amálio, Fiona Polack, Susan Stepney
• Keywords: Formal Methods, Practical Formal Verification, Schema Calculus, Structuring, ZUM 2005