Cross-Cutting Techniques in Program Specification and Analysis

paper ps
We present three aspect-oriented constructs (formats, scopes, and defaults) that, in combination with a specification language based on abstract sets of objects, enable the modular application of multiple arbitrarily precise (and therefore arbitrarily unscalable) analyses to scalably verify data structure consistency properties in sizable programs. Formats use a form of field introduction to group together the declarations of all of the fields that together comprise a given data structure. Scopes and defaults enable the developer to state certain data structure consistency properties once in a single specification construct that cuts across the preconditions and postconditions of the procedures in the system. Standard approaches, in contrast, scatter and duplicate such properties across the preconditions and postconditions. We have implemented a prototype implementation, specification, analysis, and verification system based on these constructs and used this system to successfully verify a range of data structure consistency properties in several programs. Most previous research in the field of aspect-oriented programming has focused on the use of aspect-oriented concepts in design and implementation. Our experience indicates that aspect-oriented concepts can also be extremely useful for specification, analysis, and verification.

Citation

Patrick Lam, Viktor Kuncak, and Martin Rinard. Cross-cutting techniques in program specification and analysis. In 4th International Conference on Aspect-Oriented Software Development. ACM, March 2005.

BibTex Entry

@inproceedings{LamETAL05CrossCuttingTechniquesProgramSpecificationAnalysis,
author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
title = {Cross-Cutting Techniques in Program Specification and Analysis},
booktitle = {4th International Conference on
Aspect-Oriented Software Development},
publisher = {ACM},
isbn = {1-59593-042-6},
month = {March},
year = 2005,
abstract = {
We present three aspect-oriented constructs ({\em formats}, {\em
scopes}, and {\em defaults}) that, in combination with a specification
language based on abstract sets of objects, enable the modular
application of multiple arbitrarily precise (and therefore arbitrarily
unscalable) analyses to scalably verify data structure consistency
properties in sizable programs. Formats use a form of field
introduction to group together the declarations of all of the fields
that together comprise a given data structure. Scopes and defaults
enable the developer to state certain data structure consistency
properties once in a single specification construct that cuts across
the preconditions and postconditions of the procedures in the
system. Standard approaches, in contrast, scatter and duplicate such
properties across the preconditions and postconditions. We have
implemented a prototype implementation, specification, analysis, and
verification system based on these constructs and used this system to
successfully verify a range of data structure consistency properties
in several programs.

Most previous research in the field of aspect-oriented programming has
focused on the use of aspect-oriented concepts in design and
implementation. Our experience indicates that aspect-oriented concepts
can also be extremely useful for specification, analysis, and
verification.
}
}