Premium
Better Understanding through Formal Specification
Author(s) -
Duce D. A.,
Fielding E. V. C.
Publication year - 1985
Publication title -
computer graphics forum
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.578
H-Index - 120
eISSN - 1467-8659
pISSN - 0167-7055
DOI - 10.1111/j.1467-8659.1985.tb00238.x
Subject(s) - computer science , formal specification , programming language , programmer , workstation , graphics , formal methods , language of temporal ordering specification , software requirements specification , system requirements specification , software engineering , software , software development , software design , operating system
The Graphical Kernel System (GKS) is now registered as an ISO International Standard for computer graphics programming. One of the major innovations of the Standard is the bundled specification of aspects, a mechanism which gives the applications programmer the ability to tailor the appearance of a picture independently on each of the workstations on which it is displayed, using the capabilities of the workstations. GKS also incorporates the traditional method of individual specification of aspects in which each workstation does the best it can to represent global aspect values. In this paper a formal specification technique, the Vienna Development Method (VDM), is used to describe aspect specification. The GKS model of aspect specification is progressively constructed from simpler models. Properties of these simpler models are formulated and the specifications are proved to conform to these. The properties are then traced through the more complex models. The paper demonstrates the applicability of formal specification to the design of graphics software and the ability of formal techniques to catalyse the deeper understanding of designs.