No label defined (Q4339214)

Diese Arbeit befaßt sich mit der formalen Entwicklung graphischer Benutzerschnittstellen. Ziel der Arbeit ist, bekannte (klassische) algebraische Methoden für den Entwurf von Softwaresystemen an den Entwurf von Benutzerschnittstellen anzupassen, d.h. diese Methoden entsprechend zu instantiieren und zu erweitern. Dies umfaßt Methoden für die Spezifikationen und Implementierungen der grundlegenden Komponenten, die Validierung der Spezifikationen, die Verifikation der Implementierungen, und die Wiederverwendung von Komponenten graphischer Benutzeroberflächen. Die grundlegenden Komponenten werden zunächst formal beschrieben. Die einfachen interaktiven Komponenten, wie z.B. Buttons, werden durch Zustandsübergangssysteme modelliert und dann nach SPECTRUM transformiert. Die komplizierten interaktiven Komponenten, wie z.B. Menus und Windows, werden spezifiziert durch die Anwendungen der Operatoren, die für ``specifying in the large'' in der Spezifikationssprache definiert worden sind. Die Repräsentationskomponenten, wie z.B. Display Windows und Glues, werden auch spezifiziert. Die Spezifikationen sind in der funktionellen Programmsprache SML implementiert. Das Theorembeweissystem ISABELLE wird verwendet, um die kritischen Eigenschaften von interaktiven Komponenten zu validieren. Eine Methode, basierend auf Programmtransformationstechniken und Realisierungen von Spezifikationen, wird entwickelt, um die Korrektheit der Implementierung von Spezifikationen zu verifizieren. Die Wiederverwendbarkeit von Softwarekomponenten wird in dieser Arbeit diskutiert. Eine Bibliothek von wiederverwendbaren Komponenten, die aus Spezifikationen und Implementierungen bestehen, wird entwickelt und durch Entwicklungsgraphen dargestellt. Eine operator-orientierte Methode für die systematische Wiederverwendung ist presentiert in der formalen Entwicklungen der graphischen Benutzerschnittstellen eines Editors und der Fallstudie HDMSA aus dem KORSO-Projekt.