Design Rationale

 

BSL is the latest in a series of languages and systems that we have created to support specification of temporal properties of software systems. Experience with an earlier simple property language for Ada software [5] and with a system of temporal specification patterns [7] has yielded the following design criteria that we have tried to follow as we address the challenging issues surrounding specifying properties of Java source code.

1.   The specification language must hide the intricacies of temporal logic by emphasizing common specification coding patterns.
2.   Even though details of temporal logics are to be hidden, expert users should be allowed ``back doors'' to write specifications (or fragments of specifications) directly in, e.g., LTL.
3.   The language must support specification styles that are already used by developers such as assertions, pre/post-conditions, etc.
4.   The specification artifacts themselves should be strongly connected to the code. The specifications will reference features from the code (e.g., variable names, method names, control points), so the principal specification elements should be located with the code so that developers can easily maintain them, read them for documentation, and browse them.
5.   Finally, and perhaps must importantly, the language must include support for reasoning about language features used in real software such as dynamic object/thread creation, interface definitions, exceptions, etc. These often give rise to heap-allocated structures that are reachable by following chains of object references, but are effectively anonymous when considering a Java program's static fields and local variables.

Criterion (1) derives from experience with the Specification Patterns Project. BSL provides a macro facility that implements all the patterns from [7]. Conforming to criterion (2), it also allows expert users to write their own patterns or code their temporal logic specifications directly.

Following criterion (3), the design and presentation of BSL has been influenced by various Java assertion languages such as iContract [12]. In each of these languages above, developers write their specifications in Java comments using the Javadoc facility. We have also followed this approach because it is an effective way to address criterion (4): browse-able HTML documentation for BSL specifications can be created, and the close physical proximity of comments and code encourages regular maintenance.

BSL currently does not address all the program features mentioned in criterion (5) (e.g., we don't discuss specifying properties of exceptions in this work), but it does make significant steps in handling heap-allocated data/threads.