FORMAL SPECIFICATION OF WINDOW SYSTEMS

Abstract

Window management systems are now used extensively for user interfaces to computer systems. Part I of this monograph introduces some of the fundamental ideas in window systems using a formal notation. Part II outlines three real systems and attempts to capture the essence of each system using the same formal notation and ideas introduced in Part 1. Low-level detail is avoided to keep the length to a, manageable size. In Part I, chapter 1 introduces general concepts useful for specifying pixel maps and window systems. Chapter 2 defines the raster-op function which is fundamental to many graphics operations and chapter 3 introduces a simple example window system. In Part II, chapters 4-6 detail three particular window systems. Chapter 7 remarks on experience gained by formally specifying the three window systems. The formal notation used, Z, is based on set theory, and has been developed at the Programming Research Group in Oxford.