The Bandera Specification Language

 

The previous sections have given some simple examples to illustrate the basic concepts of the Bandera Specification Language (BSL). This section gives a more indepth overview of the motivation and design rationale of the BSL, and includes a detailed discussion of BSL's syntax and semantics.

• Introduction
• Design Rationale
• The Assertion Sublanguage
  • Rationale
  • Syntax and informal semantics
  • Implementation issues
• The Temporal Specification Sublanguage
  • Predicate Definition Sublanguage
  • Syntax and informal semantics
  • Implicit Constraints
• Specifying Temporal Patterns
  • Specifying Properties for Class Instances
  • Universal Class Instance Quantification
  • Implementation Issues