Categorical Characterization of Structure Building Operations

LOPEZ POMBO, CARLOS GUSTAVO; FRIAS, MARCELO FABIÁN

Salamanca

Workshop; Worshop on Algebraic Development Techniques; 2012

Modularity is a key concepts when aiming at good designs. In [1,2], Parnas extensively discusses how modular designs of software artifacts result in higher quality software by enabling reuse, separation of concerns and better maintain- ability. Since Parnas?s foundational work, practitioners build software artifacts (and particularly software specifications), modularly. In [3], Goguen and Burstall present a categorical formalization of the abstract model theory of a logic using the formalism of institutions. Institutions provide an abstract view of a logic that enables the study of properties of a formalism independently of notational issues. For instance, [4] surveys interesting results about well-known properties such as interpolation, within the framework of institutions. In [5], Sanella and Tarlecki provide a set of structure-building operations that enable the modular construction of specifications from theories taken from a given institution. In [6], Borzyszkowski presented a logical system for the structure building operations (SBOs) introduced by Sanella and Tarlecki, as well as an extensive discussion on the conditions under which the proposed calculus is complete. Intuitively we would like to consider structured specifications as syntactically sweetened ways of describing a system whose behavior is equivalent to a monolithic non-structured specification. This is not the case in the SBOs presented in [5]. Let us recall their definition: 1) a flat specification is assumed to be a legal structured specification, 2) the union of two structured specifications over the same signature is considered as a structured specification, 3) the translation over a morphism between signatures is a structured specification, and 4) the derivation (understood as the hiding of symbols) along a signature morphism is a structured specification. In Borzyszkowski?s work two operations are defined, Sig and Mod for the retrieval of the signature and the class of models of a structured specification, respectively. Both operations, defining the semantics of the structuring mechanism, are defined inductively on the structure of the specification. Therefore, in order to preserve the idea of structure as denotation, a question arises: Is it possible to define a function assigning a flat specification to every structured one? While the problem is easily solved (positively) for specifications built from unions and translations, the class of models resulting from hiding symbols is explained as the reducts of the models of a set of axioms described in terms of symbols that no longer belong to the language. Thus, the language is not necessarily able to syntactically describe the conditions needed to impose certain structure to the models. Assume the institution under observation is a first-order language with con- junction, and that derivations only take place on constant symbols. Thus, a derived structured specification denotes a flat specification in which those axioms stating properties of a constant symbol c are replaced by a single one where a variable xc is existentially quantified as follows: {Ax1(c),...,Axk(c)} → ∃xc(Ax1(xc)∧···∧Axk(xc)) . (1) This solution can be formalized by defining a family of endo institution representations [7] indexed by an appropriate subset of signature morphisms. Hiding symbols is the formal resource for stating that a certain function is to be considered private to a software module. Thus, for a technique as the one hinted in (1) to be useful, we should be able to quantify over function symbols. Higher-order logic give us a solution at the expense of missing an effective, sound and complete calculus. In this work, given an institution I, we solve the problem of properly defining a semantics for structured specifications in terms of flat ones, by representing the underlying institution in a more expressive one U in which first-order objects provide semantics for functions in I. References Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Communications of the ACM 15(12) (1972) 1053?1058 See also [?]. Parnas, D.L.: Designing software for ease of extension and contraction. IEEE Transactions on Software Engineering 5(2) (1979) 128?138 See also [?]. Goguen, J.A., Burstall, R.M.: Introducing institutions. In Clarke, E.M., Kozen, D., eds.: Proceedings of the Carnegie Mellon Workshop on Logic of Programs. Volume 184 of Lecture Notes in Computer Science., Springer-Verlag (1984) 221?256 Tarlecki, A.: Bits and pieces of the theory of institutions. In Pitt, D.H., Abramsky, S., Poign ́e, A., Rydeheard, D.E., eds.: Proceedings of the Category Theory and Computer Programming, tutorial and workshop. Volume 240 of Lecture Notes in Computer Science., Springer-Verlag (1986) 334?363 Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and computation 76(2?3) (1988) 165?210 Borzyszkowski, T.: Completeness of a logical system for structured specifications. In Parisi-Presicce, F., ed.: Proceedings of the 12th. International Workshop on Recent Trends in Algebraic Development Techniques WADT 1997. Volume 1376 of Lecture Notes in Computer Science., Tarquinia, Italy, Springer-Verlag (June 1997) 107?121 Tarlecki, A.: Moving between logical systems. In Haveraaen, M., Owe, O., Dahl, O.J., eds.: Selected papers from the 11th Workshop on Specification of Abstract Data Types Joint with the 8th COMPASS Workshop on Recent Trends in Data Type Specification. Volume 1130 of Lecture Notes in Computer Science., Springer- Verlag (1996) 478?502