Views of queues

Starting from an algebraic specification of the data type QUEUE several variants of communicating agents representing queues are studied. It is demonstrated how new issues such as exceptions, robustness, and concurrency can be considered, when going from a purely algebraic view of queues to queues used in the framework of communicating systems. Nevertheless the verification of the communicating agents can be done by classical techniques for proving implementations correct, developed in the framework of algebraic specification. Finally the design of infinite networks representing queues and their verification is demonstrated. Although shown only for a simple example a general method is aimed at for the development of interactive and concurrent programs from algebraic specification using applicative programming styles.