Categorical foundations for structured specifications in $${\mathsf{Z}}$$Z. (November 2015)

• Record Type: Journal Article
• Authors: Castro, Pablo; Aguirre, Nazareno; Pombo, Carlos; Maibaum, T.
• Is Part Of: Formal aspects of computing. Volume 27:Number 5(2015)
• Page Start: 831
• Page End: 865
• Publication Date: 2015-11
• Subjects: Z Notation -- System specification -- System verification -- Category theory -- Heterogeneous specifications; Computer science -- Periodicals; 004.05
• DOI: 10.1007/s00165-015-0336-0
• Languages: English
• ISSNs: 0934-5043

Abstract

Abstract In this paper we present a formalization of the $${\mathsf{Z}}$$ Z notation and its structuring mechanisms. One of the main features of our formal framework, based on category theory and the theory of institutions, is that it enables us to provide an abstract view of $${\mathsf{Z}}$$ Z and its related concepts. We show that the main structuring mechanisms of $${\mathsf{Z}}$$ Z are captured smoothly by categorical constructions. In particular, we provide a straightforward and clear semantics for promotion, a powerful structuring technique that is often not presented as part of the schema calculus. Here we show that promotion is already an operation over schemas (and more generally over specifications), that allows one to promote schemas that operate on a local notion of state to operate on a subsuming global state, and in particular can be used to conveniently define large specifications from collections of simpler ones. Moreover, our proposed formalization facilitates the combination of $${\mathsf{Z}}$$ Z with other notations in order to produce heterogeneous specifications, i.e., specifications that are obtained by using various different mathematical formalisms. Thus, our abstract and precise formulation of $${\mathsf{Z}}$$ Z is useful for relating this notation with other formal languages used by the formal methods community. We illustrate this by means of a known combination of formal languages, namely the combination of $${\mathsf{Z}}$$ Z with $${\mathsf{CSP}}$$ CSP .