archives

Ownership and Effects for more Effective Reasoning about Aspects


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Clifton, Curtis, Leavens, Gary T. and Noble, James (2006) Ownership and Effects for more Effective Reasoning about Aspects. Technical Report 06-35, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

There is a later version of this eprint available: Click here to view it.

Abstract

Aspect-oriented languages like AspectJ increase the number of places in a program that need to be considered during reasoning. Advice can send messages to and write fields of any object, and can effectively override any method definition. Aspects can also interfere with other aspects. MAO is a variant of AspectJ that demonstrates how to make reasoning easier by allowing programmers, if they choose, to declare that their advice has limited control and heap effects. Heap effects, such as assignment to object fields are specified using "concern domains", which are declared heap partitions. We show, for example, how declaring what concern domains are read and written by methods and advice can be used to separate objects owned by the base program from those owned by aspects. Such concern domain annotations can also be used to check that advice cannot interfere with the base program or with other aspects. Besides allowing programmers to declare how concerns interact in a program, concern domains also support a simple kind of semantic pointcut. These features support more effective reasoning about control and heap effects.

Keywords:Aspect-oriented programming, ownership, concern domain, control effects, heap effects, heap effect dependency, writes, curbing, spectator, AspectJ language, MAO language.
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: General
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
ID code:00000494
Deposited by:Gary T. Leavens on 21 December 2006
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR06-35/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR06-35/TR.ps.gz

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu