Towards Proving Program Correctness Using Formal Specification

In this paper we illustrate the techniques of sequential refinement by convening a formal specification of an interactive editor of block structured languages into a concrete model of the editor suitable for use when implementing the editor for the Pascal language.