Accession Number : ADA256797


Title :   Aspect: A Formal Specification Language for Detecting Bugs


Descriptive Note : Master's thesis


Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE


Personal Author(s) : Jackson, Daniel


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a256797.pdf


Report Date : Jun 1992


Pagination or Media Count : 165


Abstract : 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.


Descriptors :   *COMPUTER PROGRAM VERIFICATION , *STATIC TESTS , *DEBUGGING(COMPUTERS) , DETECTION , SPECIFICATIONS , DYNAMICS , COMPUTER PROGRAMMING , PROGRAMMING LANGUAGES , PROTOTYPES , STATICS , POLYMORPHISM , COMPILERS , MODEMS , ABSTRACTS , ERRORS , LANGUAGE , ALLOCATIONS , POWER


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE