Bounded Buffer requirements

What are some of the properties we might want to check for the BoundedBuffer? And what are some of the constraints we might want to put on the BoundedBuffer? Below is a list of properties that we can check with Bandera.

1. Buffers are constructed with positive bounds.  
2. Elements are always added in correct position.  
3. Indices always stay in range.  
4. Full buffers eventually become non-full.  
5. Empty buffers must be added to before being taken from.  

In the next subsections, we discuss the BSL predicate and assertion definitions necessary for specifying each of these requirements. Then we will return to using the BUI to define appropriate sessions for checking specifications of Requirements 1 and 3.