Building a session for requirement three

 

In this section we will describe how to create a session to check requirement three: indices always stay in range.

• Open an existing session file.
• Add a new session to it by clicking on the New option of the Session Manager window. Activate the new session and name it IndexRange for instance. Click on the Compiler tab at the top of the Session Manager window and choose CompleteBoundedBuffer.java as the target file. Close the Session Manager window and click on Run on the top tool-bar to run the example through JJJC and load the code and specifications into the system.
• Click on the Property option on the second tool-bar to bring out the Property Manager window.
• The steps for creating the temporal property are similar to the steps taken for the pipeline example. Click on the Temporal Logic tab at the top, then click on Add to create a new property. Activate/Deactivate the property and give it a name, IndexRangeProp, for example.
• In the Quantifications field enter

  forall[b:BoundedBuffer].

• Remember that we are using a universal pattern with global scope for this property, so under the Proposition choose Universality and under the Pattern Scope choose Globally. Now you are ready to choose the predicate. You will need to choose only one. Choose

  BoundedBuffer.IndexRange

  predicate and add (b) at the end.
• Expand the formula to make sure it is correct
• To save the property specification to a file click on the Property tab at the top of the Property Manager window and click on Save as option at the bottom. You can either save this specification into a separate file or add it to an existing specification file, for example, the one you created in the previous section. To save into a separate file, give it new name. To save into already exisiting file you would have to edit the existing specification file using a text editor. Go ahead and save your property into a separate file.
• Dismiss the Property Manager window.
• Click on the Slicer option on upper tool-bar of the main window to use the slicer for better performance. Run the example through and browse the code to see which components get sliced away. You shoud see that as in the previous section, the slicer eliminates the buffer array. Note that for checking this property we don't want to have the second assertion enabled, as it would spoil the slicing criteria. This is a point to remember when creating sessions with multiple temporal properties and assertions enabled.
• To pick the model checker at the backend of Bandera click on the Session option of the main window and choose the Checker tab at the top of the Session Manager window. Pick the checker and dismiss the Session Manager window.
• Click on the Checker option to enable the model checker and at last click on the Run. You should get a confirmation that your property has been verified.