Aspect: A Formal Specification Language for Detecting Bugs
MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE
Pagination or Media Count:
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.
- Computer Programming and Software