A FORMAL SPECIFICATION FOR A USER INTERFACE FOR OFFICE AUTOMATION

This work describes a formal method for specifying the user interface of an Office Automation (OA) system. Since there are no standard office environments to base the formal specifications on, some components of an OA system which model the workings of many offices are considered. A model for the interface to the OA system is developed. Based upon this model the requirements of a hypothetical user is described. From these requirements components of an OA system satisfying them are identified. Formal specification techniques are described. The algebraic specification technique is used for specifying the user interface. Completeness and consistency of the algebraic specification are discussed and the notion of sufficient completeness is presented. An algorithm for testing the sufficient completeness of an algebraic specification of an abstract data type under certain constraints is discussed. Calculus of Communicating Systems is used as a formal specification technique for describing user interaction and communication aspects of the OA system. Finally a framework for the design of a user interface is considered.