Aspect: a formal specification language for detecting bugs
Daniel Jackson, John V. Guttag · Defense Technical Information Center (DTIC) · 1992
Aspect is a static analysis technique based on formal specifications. By trading expressive power for tractability, Aspect can offer efficient detection of a class of bugs that is not detectable by other static means. Since the specifications are partial, not all bugs can be caught. But there are never any spurious reports: an error message always indicates an error in the code or a flaw in the specification. Aspect can handle most of the features of modern imperative programming languages: side-effects and aliasing, exceptions, polymorphism and dynamic allocation. It takes advantage of strong typing and is designed for programs that are organized around procedures and abstract types. The checking mechanism is based on an enriched form of dependency analysis. Objects are divided into projections called 'aspects'; the dependencies of different aspects are then tracked individually. The analysis is comparable in complexity to the kinds of analysis already performed by optimizing compilers. A prototype checker has been implemented tor the CLU programming language. It runs almost as fast as the compiler, and has found a variety of bugs in real programs.