A Categorical Approach to Structuring and Promoting Z Specifications

CASTRO, PABLO; AGUIRRE, NAZARENO M.; LOPEZ POMBO, CARLOS GUSTAVO; MAIBAUM, THOMAS S.E.

LECTURE NOTES IN COMPUTER SCIENCE

Springer Verlag

Lugar: Berlín; Año: 2012 vol. 7684

0302-9743

In this paper, we study a formalisation of specification structuring mechanisms used in Z. These mechanisms are traditionally understood as syntactic transformations. In contrast, we present a characterisation of Z structuring mechanisms which takes into account the semantic counterpart of its typical syntactic descriptions, based on category theory. Our proposed formal foundation for Z employs well established abstract notions of logical systems. This setting has a degree of abstraction that enables us to understand what is the precise semantic relationship between schemas obtained from a schema operator and the schemas it is applied to, in particular with respect to property preservation. Our formalisation is a powerful setting for capturing structuring mechanisms, even enabling us to formalise promotion. Also, its abstract nature provides the rigour and flexibility needed to characterise extensions of Z and related languages, in particular the heterogeneous ones.