The first two requirements can be expressed using BSL's assertion
facility. There are three kinds of assertions in BSL: precondition,
location, and postcondition assertions.
For example, to state
Requirement 1 we can use a precondition assertion
by inserting the following
Javadoc comment immediately above the constructor method
for the BoundedBuffer class.
/**
* @assert
* PRE PositiveBound: (b > 0);
*/
The role of the tag @assert is similar to that of
observable but is used indicate that an assertion is being
defined instead of a proposition to be used in a temporal formula (the
two roles cannot be interchanged without changing the tag). The label
PRE indicates that this is the precondition assertion that
needs to hold right before we enter the constructor code. The name of
the assertion is PositiveBound.
Since we are expressing this requirement as an assertion, we do not need to instantiate a temporal pattern as we did for the requirement in the Pipeline example. Rather, Section 5.6.8 will show that we simply define a session and enable this assertion for checking.