In this thesis we define a framework for the specification
of dynamic behavior of software systems. This framework is
motivated by the state as algebra approach and the
model-oriented language Z. From the state as algebra approach
we use the idea of modeling the environment and the state
components as structures of an institution.
However, in contrast to the state as algebra approach, states in
our framework are modeled by structures from any suitable
institution not only those having of algebras as their
structures.
From Z we use the idea that environment, state spaces and
relations between state spaces are specified using the same logic
and how more complex relations can be constructed from simpler
ones by means of the schema calculus. However, we differ from Z
in that our framework can be instantiated by different
institutions, while the approach of Z can only work because of
the particular logical system used by Z.