Requirement 2 can be expressed using a post-condition
assertion for the add method. Specifically, the following
assertion declaration would be inserted immediately before the
add(Element o) method of the BoundedBuffer class.
/** * @assert * POST addPost: (head_==0) ? buffer_[bound_-1]==o : buffer_[head_-1]==o; */The assertion states that if the
head_ was zero before an
element was added to the buffer, then the element will appear in
buffer_[bound_-1], if the head_ was non-zero, then the
element will appear in buffer_[head_-1].