Wed 21 Feb
A formal framework for modularization in an imperative context
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
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
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