After you insert the specifications into your file, you can double check your work by looking in the CompleteBoundedBuffer.java file that is annotated with BSL.
Now you are ready to run the Bounded Buffer program through Bandera and check various properties that we talked about in the previous section. We will check the first requirement only in this section. We will use the complete version of the source code file, i.e. we will have assertions and predicates ready for our use.
PositiveBound for instance. Click on the Compiler tab at the top of
the Session Manager window and specify the file to be used. Make sure to use the
CompleteBoundedBuffer.java. Close the Session Manager window and run the
example through with only the JJJC option enabled on the top tool-bar of the
main window. This will load the code into Bandera which will extract assertions and
predicates specified in the file.PositiveBound. Click on the
Property option on the second tool-bar to bring out the Property Manager
window. Click on the Assertion tab at the top of the window. Click on the
Add option at the top and then on the Activate/Deactivate option in
the window. This will activate the Add button at the bottom part of the
window. Clicking on it will bring out the Enable Assertion window that will
let you choose an assertion from a set of assertions specified in the program. Choose
BoundedBuffer.BoundedBuffer.PositiveBound assertion and click on OK
button to dismiss the Enable Assertion window.PositiveBound. If you intent to keep all of
specifications in the same file, you might want to name it BoundedBuffer, for
instance. Make sure to use .specification extension for your specification
file.BoundedBuffer class. Note that the buffer array called
buffer_ has been removed from the program as well as any references to it.
Slicing will not produce similar results for the second assertion from the previous section: elements are always added in the correct position. In this case the slicer can not eliminate the buffer array since it is reffered to in the assertion. This is a very important point to remember whenever you have a few assertions inserted into the program. You might not want to have all of the assertions enabled at once for different sessions. You might want to selectively enable some of the assertions only.