A complete specification file

As we already pointed out in the previous section, a user can create temporal properties and enable/disable assertions using the BUI. However, if a user wants to save specifications on the per session basis, she might end up with many different specification files. We encorage to keep all of the specifications for the same example in the same file.

You can create all of your specifications at once using the Property Manager window and save them in one file.

Another option would be to directly write out the specifications into a file using a text editor such as Emacs.

BoundedBuffer.specification displays a single specification file that holds the property declarations for each of the five bounded buffer requirements.

The syntax for enabling multiple assertions is as follows:

  BufferAssertions: enable assertions { PositiveBound, AddToEnd };

Once you have the full specification file created and saved, use the following steps to select the property you want to check in a single session:

• Bring out the Session Manager window. Click on the Property tab at the top of the window. Click on the top Edit button to select the specification file. Opening of the file will bring out the Property Manager window.
• Use the Property Manager window to select the property. Click on the Temporal Logic tab at the top. The Property Manager window will display the set of the temporal properties wriiten in the file. Activate the property you like to check in your session.
• Make sure to check the assertions enabled. As we pointed out in the previous sections, you might not want to have all of the assertions enabled at once, as some of them might be too strict and spoil the performance of slicing, for example.
• To control the set of assertions, click on the Assertion tab at the top of the Property Manager window. Activate the set of assertions displayed in the top part of the window. You will see the set of assertions displayed individually at the bottom part of the window. Use Remove option of the bottom part of the window to remove the assertions you don't want to be checked during the execution of your session.