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.
Abstract
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
Keywords
partial specification, partial verification, dataflow dependences.