Date: Wed 21 Feb
Time: 15.00
Place: room 214

Speaker: Davide Ancona
Title: A formal framework for modularization in an imperative context

Abstract. Our work addresses the problem of defining an abstract formal framework for modular dynamic systems (i.e. systems supporting the notion of module with state). The notion of institution has been intensively used for modeling specifications and specification composition and has proved the importance of the categorical approach for giving an abstract characterization of some fundamental composition operations over specifications. On the other hand, several efforts have been spent for extending the well-known notion of (abstract) data-type to the imperative context, by following the ``state-as-algebra'' approach. We intend to follow both these two approaches in order to develop our framework. A module with state is interpreted as a mathematical structure (a dynamic data-type) over a given dynamic signature; a dynamic data-type consists in a set of states which are algebras and a family of dynamic operations which are transformations of algebras. The notions of dynamic data-type and dynamic signature are parameterized over the algebraic framework (called static framework) chosen for modeling states and lead to the definition of the model part of an institution. Some general properties of this model part ensure the existence of composition operations like renaming, hiding and disjoint union with sharing; of course these properties depend also on the static framework. As a consequence, when instantiated by an appropriate static framework, our proposed framework provides a semantics driven kernel language for module expressions and a corresponding compositional semantics.