Our objective with this chapter is to outline and demonstrate the main specification and development techniques of Focus. The chapter is organized as a guided tour through the Focus method. We briefly explain the most central concepts and notations, we demonstrate the specification and refinement techniques, and we show that Focus Supports a classical stepwise development. Since the task of this chapter is to give a first introduction to FOCUS, the examples are simple, but nevertheless typical for interactive Systems. They all deal with the specification and implementation of unbounded buffers. An unbounded buffer is a queue that can stOre an unbounded number of data elements and return them upon request in the order they arrived.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
- A Guided Tour
- Springer New York