home > publications > Z | OO > An Object-Oriented Structuring for Z based on Views

Nuno Amálio, Fiona Polack, Susan Stepney
An Object-Oriented Structuring for Z based on Views.

In ZB2005: Fourth International Conference of B and Z Users, Guildford, UK, April 2005 . LNCS 3455, pp 262-278. Springer, 2005.

Abstract:

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
)