[
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
http://www.cse.ohio-state.edu/~khatchad