Refinement

Chapters 5 through 13 have presented all the description techniques and specification styles that are supported by FOCUS. To make proper use of this specification formalism in a system development process we need a clear understanding of what it means for a specification or a program to refine or implement another specification. In the guided tour of Chapter 2 we already touched on this matter. In this and the following three chapters, we introduce, explain, and define refinement in a much more careful manner.