Formal specification and verification of graphical user interfaces

A technique for the fully formal specification and verification of graphical user interfaces is described. The technique is based on the algebraic specification of abstract datatypes. Both application program and user interface are defined in the same form, using equational axioms to specify formal semantics. The relationship between an application and its interface is defined using display axioms that specify the connection between abstract application operations and the corresponding operations of the interface. Using these display axioms, one can formally verify that an interface is correct with respect to the underlying application. In addition, the display axioms can be treated as a form of executable specification, used at runtime to maintain correspondence between the application program and its interface