A Case Study: the Ferry Problem
In most articles on algebraic specifications trivial examples like stacks, queues and sets are used [Goguen78, Guttag78]. As an unbounded stack does not exist in reality, it seems cooked up by the algebraicists because it suits their approach so well. Actually, examples like stacks, queues and sets are useful to illustrate the basic principles of algebraic specifications to those who want to have a first impression. As for programming in the small versus programming in the large, techniques and notations for designing small specifications do not necessarily apply to large ones. In Chapters 5 and 6, we deal with examples of a degree of complexity which is representative for large specifications. It is our intention to show that algebraic specifications, as described in the previous chapters, are appropriate not only for small examples but also for non-trivial case studies.
Unable to display preview. Download preview PDF.