Specifying a visual file system in Z
John Hughes · Formal Methods · 1989
Part of the system software of a well-known range of personal computers with a direct manipulation user interface is specified. This software is referred to as product M, and the computers as product A. Product M provides a visual interface to a hierarchical file system. Files, discs, and folders (directories) are visible as icons on the screen. They may be moved or copied from place to place by dragging their icons around with the mouse. Dragging an icon into the 'trash can' discards it. Discs and folders may be 'opened', creating a window on the screen in which their contents can be viewed. These aspects of product M are specified using the Z specification language and the specification style developed at Oxford. The specification begins with a very abstract description of product M, to which more detail is added step by step. The Z schema calculus is used to build more detailed specifications from simpler ones, and to combine several detailed views to make the complete specification. This allows the specification of a relatively complex system to be built up from several simple parts, each specifying one aspect of the overall system. The specification technique used was inspired by Sufrin's specification of an electronic mail system (B.A. Sufrin). >