Formal specification of bounded buffer using stream functions

Formal specifications of software components are critical to software development. Several types of formal or semi-formal methods are commonly used for software specification, such as specification languages, graphic diagrams, algebraic descriptions, and stream functions. Each of these methods addresses the specification problem from a different view point and has its own strengthens and weaknesses. In this paper, we use the stream function approach to formally specify a particular software component, bounded buffer. Based on the specification, a state transition machine is built as an implementation of the bounded queue.