Property Specification Buttons

The next four buttons on the lower tool bar are associated with property specification.

• The Assertion button invokes the Assertion Browser which allows you to browse the assertions that you have declared in the code specified by the current session.
• The Predicate button invokes the Predicate Browser which allows you to browse the predicates (observables) that you have declared in the code specified by the current session.
• The Pattern button invokes the Pattern Manager. Recall that Bandera's temporal specification language is based on a collection of temporal specification patterns. The Pattern Manager allows the user to browse the patterns, and to add, modify or remove patterns. Typically, only expert users will change the collection of patterns.
• The Property button invokes the Property Manager which allows the user to specify properties to be checked for the code specified by the current session.