Relations between abstract datatypes modeled as abstract datatypes

Abstract

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.

In dieser Arbeit schlagen wir einen Ansatz zur Spezifikation des Verhaltens von Softwaresystemen vor. Dieser Ansatz ist motiviert durch Spezifikationssprachen, die den Zustand von Softwaresystemen als Algebren modellieren, und durch die modellorientierte Spezifikationssprache Z. Von der ersten Gruppe von Spezifikationssprachen übernehmen wird das Konzept den Zustand als Struktur einer Logik zu modellieren; allerdings ist unser Ansatz nicht auf Logiken beschränkt, deren Struktur Algebren sind. Von Z übernehmen wir die Idee Zustandsräume und Zustandsübergänge mit derselben Logik zu spezifizieren, und die Art und Weise wie aus einfachen Zustandsräumen und Zustandsübergängen komplexere Zustandsräume und Zustandsübergänge konstruiert werden können. Im Gegensatz zu Z können wir eine beliebige Logik verwenden, während der Ansatz von Z nur funktioniert weil eine ganz spezielle Logik verwendet wird.