Abstract analysis with aspect
Daniel Jackson · 1993
Aspect is a static analysis technique for detecting bugs in code based on three forms of abstraction: declarative specification, data abstraction and partiality (ignoring some behavioural details). Together, they bring efficiency (the checker runs almost as fast as a type checker), modularity (a procedure can be analysed independently of the procedures it calls) and incrementality (allowing the checking of incomplete programs). Aspect can detect errors that are not detectable by other static means, especially errors of omission, which are pervasive but usually hard to detect.