Deriving different views of an interactive double-ended bounded queue

We derive different views of an interactive double-ended bounded queue in the setting of stream processing functions. The views describe major abstraction levels relevant for the stepwise design of an implementation. The external view models the input/output behaviour, the internal view reflects a state-based description, the trace view presents an event-based characterization. The different views are systematically derived from the external view following sound transformation rules. The case study exemplifies formal methods for the systematic refinement of interactive components.