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 template-instantiation approach to expressing OO models in Z; practical formal verification and validation of the model can be undertaken using meta-proof, meta-lemmas, and formal snapshots.
Full paper : PDF 241K
@inproceedings(SS-ZB-05a, author = "Nuno Am\'{a}lio and Fiona Polack and Susan Stepney", title = "An Object-Oriented Structuring for {Z} based on Views", pages = "262-278", crossref = "ZB-05" ) @proceedings(ZB-05, title = "ZB2005: Fourth International Conference of B and Z Users, Guildford, UK, April 2005", booktitle = "ZB2005: Fourth International Conference of B and Z Users, Guildford, UK, April 2005", editor = "Helen Treharne and Steve King and Martin Henson and Steve Schneider", series = "LNCS", volume = 3455, publisher = "Springer", year = 2005 )