Aspect: Detecting Bugs with Abstract Dependences

Author: Daniel Jackson

Proceedings of the ACM Transactions on Software Engineering and Methodology, April, 1995.

Sorry, no postscript available.


Aspect is a static analysis technique for detecting bugs in imperative programs, consisting of an annotation language and a checking tool. Like a type declaration, an Aspect annotation of a procedure is a kind of declarative, partial specification that can be checked efficiently in a modular fashion. But instead of constraining the types of arguments and results, Aspect specifications assert dependences that should hold between inputs and outputs. The checker uses a simple dependence analysis to check code against annotations, and can find bugs automatically that are not detectable by other static means, especially errors of omission, which are common but resistant to type checking. This paper explains the basic scheme and shows how it is elaborated to handle data abstraction and aliasing.

Categories and subject descriptors: D.2.4 [Software Engineering]: Program verification - assertion checkers; D.2.2 [Software Engineering]: Tools and Techniques - modules and interfaces; D.2.5 [Software Engineering]: Testing and Debugging - symbolic execution; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - assertions, mechanical verification, pre- and post-conditions; D.3.3 [Programming Languages]: Language Constructs and Features - abstract data types.

General terms

verification, languages, documentation


partial specification, partial verification, dataflow dependences.