FORMAL SPECIFICATION OF A DISPLAY EDITOR

Abstract

We present a formalisation of the design of a Display Editor. The formalisation is rigorous enough to serve as a touchstone for the correctness or implementations of the editor and to permit various desirable properties of the design to be proven. The formalisation is expressed in (slightly embellished) conventional mathematical notation. The specialised features or which are explained in the text. In a companion paper [Sufrin 8lb] we give criteria by which the correctness of implementations may be judged and demonstrate how an implementation can be developed from the specification and shown to satisfy the correctness criteria.