A Categorical Approach to Structuring and Promoting Z Specifications

PABLO F. CASTRO; NAZARENO AGUIRRE; CARLOS LOPEZ POMBO; T.S.E. MAIBAUM

LECTURE NOTES IN COMPUTER SCIENCE

Springer Verlag

Lugar: Berlin; Año: 2013 vol. 7684 p. 73 - 91

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 their typical syntactic descriptions, based on category theory. Our 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.