Abstract Semantics for K Module Composition

From FSL
Jump to: navigation, search



Abstract Semantics for K Module Composition
Codruta Girlea and Grigore Rosu
K'11, ENTCS 304, pp 127-149. 2014
Abstract. A structured K definition is easier to write, understand and debug than one single module containing the whole definition. Furthermore, modularization makes it easy to reuse work between definitions that share some principles or features. Therefore, it is useful to have a semantics for module composition operations that allows the properties of the resulting modules to be well understood at every step of the composition process. This paper presents an abstract semantics for a module system proposal for the K framework. It describes K modules and module transformations in terms of institution-based model theory introduced by Goguen and Burstall.
PDF, K, DOI, K'11, BIB


Towards a Module System for K
Mark Hills and Grigore Rosu
WADT'08, LNCS 5486, pp 187-205. 2009
Abstract. Research on the semantics of programming languages has yielded a wide array of notations and methodologies for defining languages and language features. An important feature many of these notations and methodologies lack is modularity: the ability to define a language feature once, insulating it from unrelated changes in other parts of the language, and allowing it to be reused in other language definitions. This paper introduces ongoing work on modularity features in K, an algebraic, rewriting logic based formalism for defining language semantics.

Dahl Festschrift

Composing Hidden Information Modules over Inclusive Institutions 
Joseph Goguen and Grigore Rosu
Dahl's Festschrift, LNCS 2635, pp 96-123. 2004
PDF, DOI, Dahl's Festschrift, BIB

Precursor 2000 TR at UCSD

Abstract Semantics for Module Composition
Grigore Rosu
Technical Report http://roger.ucsd.edu/record=b7304233~S9, May 2000
Abstract. Programmers and software engineers agree in unanimity that a useful characteristic of the programming languages they use for implementations (C++, Java, etc.) is their support for both {\em public} and {\em private} features (types, functions). The public features are often called {\em interfaces}. The private part is not visible outside the module (class, package) that declares it, but it can be used internally to define the visible part. Such distinction helps software engineers abstract their work and ignore details which are a main source of confusion and errors. We claim that the distinction between private and public features might also be a desirable characteristic of formal specifications, not only from the practical point of view but also because of at least two important theoretical reasons. One is the possibility to finitely specify theories which do not admit finite standard presentations. For example, Bergstra and Tucker showed that any recursive algebra is a restriction of an initial algebra presented by a finite number of equations over a larger signature. Another reason is that it allows the user to specify behavioral properties of systems, in the sense that every behavioral specification is equivalent to hiding some operators (i.e., making them private) in a usual specification. We introduce the notion of {\em module specification} as a generalization of the standard specification, having both public (or visible) and private features, and then explore their properties at an abstract level, categorical. To formalize the notion of ``logical system we use {\em institutions} enriched with {\em inclusions}, an abstraction of the natural notion of inclusion of signatures from particular logics. The {\em visible theorems} (or the visible consequences) of a module are those theorems which contain only visible symbols, and a model of that module is a model of its visible consequences. Five basic operations on module specifications are explored: renaming, hiding, enriching, aggregation and parameterization. An internal property of modules, {\em conservativeness}, seems to have a decisive role in giving semantics for module composition.

Personal tools