This thesis deals with issues in the interplay between two important fields of research in computer science: Graphical user interfaces (GUIs) and formal techniques in software engineering. The methodology developed for the design of correct software is applied to the framework of the formal development of GUIs by instantiating some techniques and methods in the specification, implementation, verification, and reuse of standard GUI components.
In this thesis attention is paid to the formal development of standard GUI components. Simple interaction components, like buttons, are modeled by a state transition system and later transformed to specifications in the specification language Spectrum. Complex interaction components, like menus and win-dows, are specified using the operators defined for »specifying in the large« in Spectrum. Representation components, like display windows and glues, are also specified in this way. The specifications are implemented in the functional programming language Sml.
The properties of some components are validated using the theorem proof system Isabelle based on the axioms of their specifications. To verify programs satisfying the abstract specifications, a verification method related to program transformation and specification realization is developed.
The issues of software component reuse are also discussed in this work. A library of reusable components consisting of both specifications and programs (codes) is developed and is depicted by a development graph. An operator-based approach for the systematic reuse is indicated by the formal development of an eXene-based graphical editor and the Korso project case study HDMS-A.
This work supports the correct development of the programs in which graphical user interfaces are embedded.