Enforcing Behavioral Constraints in Evolving Aspect-Oriented Programs
•Download as KEY, PDF•
0 likes•548 views
Reasoning, specification, and verification of Aspect-Oriented (AO) programs presents unique challenges especially as such programs evolve over time. Components, base-code and aspects alike, may be easily added, removed, interchanged, or presently unavailable at unpredictable frequencies. Consequently, modular reasoning of such programs is highly attractive as it enables tractable evolution, otherwise necessitating that the entire program be reexamined each time a component is changed. It is well known, however, that modular reasoning about AO programs is difficult. In this paper, we present our ongoing work in constructing a rely-guarantee style reasoning system for the Aspect-Oriented Programming (AOP) paradigm, adopting a trace-based approach to deal with the plug-n-play nature inherent to these programs, thus easing AOP evolution.
Recommended
More Related Content
Viewers also liked
Viewers also liked (14)
Similar to Enforcing Behavioral Constraints in Evolving Aspect-Oriented Programs
Similar to Enforcing Behavioral Constraints in Evolving Aspect-Oriented Programs (20)
More from Raffi Khatchadourian
More from Raffi Khatchadourian (20)
Recently uploaded
Recently uploaded (20)
Enforcing Behavioral Constraints in Evolving Aspect-Oriented Programs
- 1. Enforcing Behavioral Constraints in Evolving Aspect-Oriented Programs Raffi Khatchadourian1*, Johan Dovland2, and Neelam Soundarajan1 1The Ohio State University, USA 2University of Oslo, Norway *Partially administered during visit to Lancaster University, UK
- 2. Introduction
- 3. Introduction • AOP enables modular implementation of cross- cutting concerns.
- 4. Introduction • AOP enables modular implementation of cross- cutting concerns. • Both formal and informal reasoning about AOP presents unique challenges especially in respect to evolution.
- 5. Introduction • AOP enables modular implementation of cross- cutting concerns. • Both formal and informal reasoning about AOP presents unique challenges especially in respect to evolution. • As components enter, exit, and re-enter software, conclusions about behavior of components may be invalidated.
- 6. C
- 7. A C
- 8. A C
- 9. A C
- 10. A C Behavior of C+A
- 13. C Behavior of C+A
- 14. C
- 15. What We Want
- 16. What We Want • Desire a compositional reasoning approach, however the invasive nature of AOP makes this difficult.
- 17. What We Want • Desire a compositional reasoning approach, however the invasive nature of AOP makes this difficult. • In the worst case, changes made to a single component require reexamining the entire program.
- 18. Questions
- 19. Questions • Can we draw meaningful conclusions about component code without considering the actual advice code?
- 20. Questions • Can we draw meaningful conclusions about component code without considering the actual advice code? • Can we specify the behavior of components without any particular advice in mind?
- 21. Questions • Can we draw meaningful conclusions about component code without considering the actual advice code? • Can we specify the behavior of components without any particular advice in mind? • Can we parameterize specifications over all possibly applicable aspects?
- 22. Questions • Can we draw meaningful conclusions about component code without considering the actual advice code? • Can we specify the behavior of components without any particular advice in mind? • Can we parameterize specifications over all possibly applicable aspects? • Can we suitably constrain the behavior of aspects as the software evolves?
- 24. Hiding Behind Interfaces • Using interface is one answer (e.g., XPIs, Open Modules)
- 25. Hiding Behind Interfaces • Using interface is one answer (e.g., XPIs, Open Modules) • But it would be nice to have a way to derive the enriched behavior of the base plus the aspects at compile time.
- 26. Insight
- 27. Insight • AO programs inherently enjoy plug-n-play capabilities [Laddad03]
- 28. Insight • AO programs inherently enjoy plug-n-play capabilities [Laddad03] • Crosscutting features can be plugged-in to enrich the behavior of advised components.
- 29. Insight • AO programs inherently enjoy plug-n-play capabilities [Laddad03] • Crosscutting features can be plugged-in to enrich the behavior of advised components. • Likewise, can we specify components so that we can derive their behaviors in a similar fashion?
- 30. C
- 31. Spec(C) C
- 32. Spec(C) C
- 33. Spec(C) C
- 34. Spec(C) A1 C A2
- 35. Spec(C) Spec(A1 ) Spec(A2 ) A1 C A2
- 36. Spec(A1 ) Spec(C) Spec(A2 )
- 37. Spec(A1 ) Spec(C) Spec(A2 ) Compose Behavior of C+A1
- 38. Spec(A1 ) Spec(C) Spec(A2 ) Compose Compose Behavior of C+A1 Behavior of C+A2
- 39. Spec(A1 ) Spec(C) Spec(A2 ) Compose Compose Compose Behavior of C+A1 Behavior of C+A1+A2 Behavior of C+A2
- 40. Obstacles
- 42. Obstacles • Usefulness • Is it possible to draw meaningful conclusions from such incomplete information?
- 43. Obstacles • Usefulness • Is it possible to draw meaningful conclusions from such incomplete information? • Obliviousness
- 44. Obstacles • Usefulness • Is it possible to draw meaningful conclusions from such incomplete information? • Obliviousness • Specifications contain “slots” for applications of crosscutting concerns.
- 45. Obstacles
- 47. Obstacles • Abstraction • Competing forces:
- 48. Obstacles • Abstraction • Competing forces: • Specs abstract internal details components, aspects directly manipulate them.
- 49. Obstacles • Abstraction • Competing forces: • Specs abstract internal details components, aspects directly manipulate them. • Composition
- 50. Obstacles • Abstraction • Competing forces: • Specs abstract internal details components, aspects directly manipulate them. • Composition • Which pegs go into which holes?
- 51. Obstacles • Abstraction • Competing forces: • Specs abstract internal details components, aspects directly manipulate them. • Composition • Which pegs go into which holes? • How to deal with dynamic and lexical pointcuts?
- 52. Obstacles • Abstraction • Competing forces: • Specs abstract internal details components, aspects directly manipulate them. • Composition • Which pegs go into which holes? • How to deal with dynamic and lexical pointcuts? • Complexity
- 53. Obstacles • Abstraction • Competing forces: • Specs abstract internal details components, aspects directly manipulate them. • Composition • Which pegs go into which holes? • How to deal with dynamic and lexical pointcuts? • Complexity • What if no advice is applicable?
- 55. Tackling Specification Complexity • May need to make assumptions about the behavior of evolving components.
- 56. Tackling Specification Complexity • May need to make assumptions about the behavior of evolving components. • Specification pointcuts
- 57. Tackling Specification Complexity • May need to make assumptions about the behavior of evolving components. • Specification pointcuts • Pointcut interfaces [Gudmundson01] annotated with behavioral specifications.
- 58. Tackling Specification Complexity • May need to make assumptions about the behavior of evolving components. • Specification pointcuts • Pointcut interfaces [Gudmundson01] annotated with behavioral specifications. • “Exported” internal semantic events within the component.
- 59. Tackling Specification Complexity • May need to make assumptions about the behavior of evolving components. • Specification pointcuts • Pointcut interfaces [Gudmundson01] annotated with behavioral specifications. • “Exported” internal semantic events within the component. • Adopt a rely-guarantee approach [Xu97] from concurrent programming to constrain the behavior of all possibly applicable advice using a rely clause.
- 60. Tackling Specification Complexity • May need to make assumptions about the behavior of evolving components. • Specification pointcuts • Pointcut interfaces [Gudmundson01] annotated with behavioral specifications. • “Exported” internal semantic events within the component. • Adopt a rely-guarantee approach [Xu97] from concurrent programming to constrain the behavior of all possibly applicable advice using a rely clause. • A guar clause may be used to constrain components.
- 61. Review of R/G for AOP [Khatchadourian07, Soundarajan07] the set of all variables of σ the program states in which each σi , σj , ... variable has a particular value
- 63. !1 !2 !3
- 66. !1 Aspect !2' !3
- 68. !a Aspect !b
- 69. The state at a point in the execution of a component is σa. !a Aspect !b
- 70. The state at a point in the execution of a component is σa. !a Aspect !b The state when the class gets control back from an aspect is σb.
- 71. The state at a point in the execution of a component is σa. !a Aspect rely(σa, σb) !b The state when the class gets control back from an aspect is σb.
- 72. Rely() Example rely(σ, σ ) ≡ (σ = σ )
- 73. Rely() Example The entire state of C rely(σ, σ ) ≡ (σ = σ )
- 74. Rely() Example rely(σ, σ ) ≡ (σ = σ ) le y ab an lic g pp kin e! y a ma tat an s om he s id fr t rb e o ic in F v es a d ang ch
- 75. Rely() Example This is “Harmless”[D&W POPL’06] rely(σ, σ ) ≡ (σ = σ )
- 77. Deriving Effective Behavior • Constraining parameterized behavior reduces complexity, but ...
- 78. Deriving Effective Behavior • Constraining parameterized behavior reduces complexity, but ... • How are formal parameters expressed?
- 79. Deriving Effective Behavior • Constraining parameterized behavior reduces complexity, but ... • How are formal parameters expressed? • How are actual parameters deduced?
- 80. Deriving Effective Behavior • Constraining parameterized behavior reduces complexity, but ... • How are formal parameters expressed? • How are actual parameters deduced? • How are the specifications composed?
- 81. Deriving Effective Behavior • Constraining parameterized behavior reduces complexity, but ... • How are formal parameters expressed? • How are actual parameters deduced? • How are the specifications composed? • Aspects are typically used to enrich the behavior of the an underlying component.
- 82. Deriving Effective Behavior • Constraining parameterized behavior reduces complexity, but ... • How are formal parameters expressed? • How are actual parameters deduced? • How are the specifications composed? • Aspects are typically used to enrich the behavior of the an underlying component. • Thus, we want to deriving the actual behavior of components with the aspects.
- 84. Join Point Traces • A Join Point Trace (JPT) variable is introduced to track the flow-of-control through various join points within a component.
- 85. Join Point Traces • A Join Point Trace (JPT) variable is introduced to track the flow-of-control through various join points within a component. • A JPT is used as a parameter over the actions of all possibly applicable aspects.
- 86. Join Point Traces • A Join Point Trace (JPT) variable is introduced to track the flow-of-control through various join points within a component. • A JPT is used as a parameter over the actions of all possibly applicable aspects. • Method post-conditions will references to the JPT.
- 87. Join Point Traces • A Join Point Trace (JPT) variable is introduced to track the flow-of-control through various join points within a component. • A JPT is used as a parameter over the actions of all possibly applicable aspects. • Method post-conditions will references to the JPT. • Informally, a JPT is used to refer to the actions and resulting values taken by advice at certain join point.
- 88. Elements of the JPT
- 89. Elements of the JPT • The JPT is composed of several components that are associated with each join point.
- 90. Elements of the JPT • The JPT is composed of several components that are associated with each join point. • Just as there are different kinds of join points (e.g., call, execution), there different kinds of JPT entries.
- 91. JPT Method Call Completion Element (oid , mid , aid , args, res, σ, σ )
- 92. JPT Method Call Completion Element (oid , mid , aid , args, res, σ, σ ) Called Object
- 93. JPT Method Call Completion Element Called Method (oid , mid , aid , args, res, σ, σ ) Called Object
- 94. JPT Method Call Completion Element Called Method (oid , mid , aid , args, res, σ, σ ) Applicable Called Object Aspect
- 95. JPT Method Call Completion Element Called Argument Method Values (oid , mid , aid , args, res, σ, σ ) Applicable Called Object Aspect
- 96. JPT Method Call Completion Element Called Argument Method Values (oid , mid , aid , args, res, σ, σ ) Applicable Method Called Object Return Value Aspect
- 97. JPT Method Call Completion Element σ, σ
- 98. JPT Method Call Completion Element State Vectors σ, σ
- 99. JPT Method Call Completion Element State Vectors σ, σ σ[oid] State of object oid after completion of method mid
- 100. JPT Method Call Completion Element State Vectors σ, σ σ[oid] State of object oid after completion of method mid σ [oid] State of object oid after completion of aspect aid
- 101. JPT Method Call Completion Element State Vectors σ, σ σ[oid] State of object oid after completion of method mid σ [oid] State of object oid after completion of aspect aid No applicable advice =⇒ σ = σ
- 102. Rule for method specification
- 103. Rule for method specification Normal pre-condition
- 104. Rule for method specification Post-condition, may include references to portions of JPT
- 105. Rule for method specification R/G Clauses
- 106. Rule for method specification
- 107. Rule for method specification
- 108. Rule for method specification Invocation of C.m on the local JPT
- 109. Rule for method specification
- 110. Rule for method specification
- 111. Rule for method specification Classic Hoare Triple
- 112. Rule for method specification
- 113. Rule for method specification
- 114. Rule for method specification Don’t forget about the guarantee
- 115. Rule for method specification
- 116. Rule for method specification
- 117. Rule for method specification If when q holds and applicable advice behaves properly implies that ...
- 118. Rule for method specification
- 119. Rule for method specification
- 120. Rule for method specification ... our post- condition holds with a a new entry in the local JPT
- 121. Rule for method specification Not sure which aspect is applicable yet, so we’ll leave this blank
- 122. Rule for method specification Replace all occurrences of σ with σ’
- 123. Rule for Method Calls
- 124. Rule for Method Calls
- 125. Rule for Method Calls Substitute actuals for formals
- 126. Rule for Method Calls
- 127. Rule for Method Calls
- 128. Rule for Method Calls Local JPT for caller
- 129. Rule for Method Calls Local JPT for callee
- 130. Rule for Method Calls Substitute formals for actuals
- 131. Rule for Aspect Application (Simple)
- 132. Rule for Aspect Application (Simple) Base-code plus an aspect
- 133. Rule for Aspect Application (Simple) Base-code pre-condition
- 134. Rule for Aspect Application (Simple) Aspect pre- condition
- 135. Rule for Aspect Application (Simple) Base-code post-condition
- 136. Rule for Aspect Application (Simple) Aspect post- condition
- 137. Rule for Aspect Application (Simple)
- 138. Rule for Aspect Application (Simple) Base-code satisfies guar
- 139. Rule for Aspect Application (Simple) Advice body
- 140. Rule for Aspect Application (Simple) State vector immediately prior to the execution of the advice
- 141. Rule for Aspect Application (Simple)
- 142. Conclusion
- 143. Conclusion • On-going work (hopefully thesis worthy! ;) )
- 144. Conclusion • On-going work (hopefully thesis worthy! ;) ) • Complete formal model (suggestions here?)
- 145. Conclusion • On-going work (hopefully thesis worthy! ;) ) • Complete formal model (suggestions here?) • Sound axiomatic proof system
- 146. Conclusion • On-going work (hopefully thesis worthy! ;) ) • Complete formal model (suggestions here?) • Sound axiomatic proof system • Curbing notational complexity via predicates.
- 147. Conclusion • On-going work (hopefully thesis worthy! ;) ) • Complete formal model (suggestions here?) • Sound axiomatic proof system • Curbing notational complexity via predicates. • Integration with IDE/theorem provers.
- 148. Conclusion • On-going work (hopefully thesis worthy! ;) ) • Complete formal model (suggestions here?) • Sound axiomatic proof system • Curbing notational complexity via predicates. • Integration with IDE/theorem provers. • Complement the Eclipse AJDT with a behavioral cross reference view?
- 149. Conclusion • On-going work (hopefully thesis worthy! ;) ) • Complete formal model (suggestions here?) • Sound axiomatic proof system • Curbing notational complexity via predicates. • Integration with IDE/theorem provers. • Complement the Eclipse AJDT with a behavioral cross reference view? • Integration with languages (e.g., via annotated pointcuts, JML)