Specifications

During the guided tour of Chapter 2 we demonstrated the various specification techniques of FOCUS. In particular, we distinguished between a number of frames and styles for writing specifications. Each frame and style has application areas in a system development where it is particularly suited. Any FOCUS specification can be syntactically transformed into a standard FOCUS specification describing the required behavior directly by a logical formula on timed streams. Thus, the frames and styles do not increase the expressive power of FOCUS, but help to improve the structure and readability of specifications.