[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] [List Home]
[aspectj-users] Survey question: Properties AO programmers are interested in verifying

(apologies for multiple posts)

Hello everyone,

I am currently working on reasoning issues in AO software and I was
wondering if I could get some feedback on the sorts of properties AO
programmers are interested in verifying about their software (thanks to
Gary Leavens for the idea!). Personally, there are four high-level
questions/scenarios that come to mind:

1) My baseline system performs as desired but aspects are being used to
    enhance or enrich that system, perhaps to provide for additional
    features and functionality. Given that aspects have been added to
    augment the baseline system, does my system still behave as desired
    despite the augmentation?

2) I am developing more or less a library aspects with no particular or
    perhaps an ideal baseline system in mind. As such, my aspects seem to
    be correct without consulting the actual systems they will be applied
    to (in fact, they may not even exist yet or I may not have access to
    them). Will applying my aspects to actual baseline systems preserve
    their correctness under my assumptions?

3) I am developing both aspects and base-code together. The baseline
    system's functionality seems incomplete without the application of
    the aspects. Similarly, the desired functionality of my aspects
    somehow depend on the behavior of the base-code they advise (e.g.,
    calls to proceed()), and consequently the aspects are also considered
    "incomplete". Would composing the aspects with the baseline system
    exhibit the desired functionality, i.e., will they complement each
    other adequately?

4) Applying a single aspect A1 to a baseline system B seems to produce
    the desired functionality, i.e., B +  A1 seems correct. Applying
    another aspect A2 to B also seems to produce desired functionality
    (perhaps the aspects are providing additional features such as in
    question 1), i.e., B + A2 seems correct. Would the desired
    functionality still be exhibited by the augmented system if I
    composed both aspects together with the baseline system
    simultaneously, i.e., B + A1 + A2, or would the aspects somehow
    conflict with each?

As previously mentioned, these are sort of higher-level properties of
the overall system. I am sure there are many more specific properties
that one may want to verify in AO software. Any feedback to this
question would be greatly appreciated and thank you for your time!

Raffi Khatchadourian
Graduate TA Lecturer/Researcher
Department of Computer Science and Engineering
The Ohio State University
Current on visitation at the Computing Department of Lancaster
University, UK