Abstract
Implicit invocation languages, like aspect-oriented languages, automate the Observer pattern, which decouples subjects (base code) from handlers (advice), and then compound them together in the final system. For such languages, event types have been proposed as a way of further decoupling subjects from handlers. In Ptolemy, subjects explicitly announce events at certain program points, and pass the announced piece of code to the handlers for its eventual execution. This implies a mutual dependency between subjects and handlers that should be considered in verification; i.e., verification of subject code should consider the handlers and vice versa.
However, in Ptolemy the event type defines only one obligation that both the handlers and the announced piece of code must satisfy. This limits the flexibility and completeness of verification in Ptolemy. That is, some correct programs cannot be verified due to specification mismatches between the announced code and the handlers’ code. For example, when the announced code does not satisfy the specification of the entire event and handlers must make up the difference, or when the announced code has no effect, imposing a monotonic behavior on the handlers.
In this paper we propose an extension to the specification features of Ptolemy that explicitly separates the specification of the handlers from the specification of the announced code. This makes verification in our new language PtolemyRely more flexible and more complete, while preserving modularity.
Chapter PDF
Similar content being viewed by others
References
Akai, S., Chiba, S.: Method shelters: avoiding conflicts among class extensions caused by local rebinding. In: AOSD ’12: Proceedings of the 11th annual international conference on Aspect-oriented Software Development, pp. 131–142. ACM Press, New York (2012)
Bagherzadeh, M., Rajan, H., Leavens, G.T.: Translucid contracts for aspect-oriented interfaces. In: FOAL ’10: Workshop on Foundations of Aspect-Oriented Languages workshop, March 2010, pp. 5–14 (2010)
Bagherzadeh, M., Rajan, H., Leavens, G.T., Mooney, S.: Translucid contracts: expressive specification and modular verification for aspect-oriented interfaces. In: Proceedings of the 10th International Conference on Aspect-oriented Software Development, AOSD ’11, pp. 141–152. ACM, New York (2011)
Bodden, E.: Closure Joinpoints: Block joinpoints without surprises. In: Proceedings of the 10th International Conference on Aspect-oriented Software Development, AOSD ’11, pp. 117–128. ACM, New York (2011)
Eric Bodden, Éric Tanter, and Milton Inostroza. Joint point interfaces for safe and flexible decoupling of aspects. ACM Transactions on Software Engineering and Methodology (TOSEM), To appear (2013)
Fernando, R.D., Dyer, R., Rajan, H.: Event type polymorphism. In: Proceedings of the eleventh workshop on Foundations of Aspect-Oriented Languages, FOAL ’12, pp. 33–38. ACM, New York (2012)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580, 583 (1969)
Inostroza, M., Tanter, É., Bodden, E.: Join point interfaces for modular reasoning in aspect-oriented programs. In: ESEC/FSE ’11: Joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 508–511 (2011)
Khatchadourian, R., Soundarajan, N.: Rely-guarantee approach to reasoning about aspect-oriented programs. In: SPLAT ’07: Proceedings of the 5th workshop on Engineering properties of languages and aspect technologies, Vancouver, British Columbia, Canada, p. 5. ACM Press, New York (2007)
Kiczales, G., Mezini, M.: Aspect-oriented programming and modular reasoning. In: Proc. of the 27th International Conference on Software Engineering, pp. 49–58. ACM Press, New York (2005)
Ongkingco, N., Avgustinov, P., Tibble, J., Hendren, L., de Moor, O., Sittampalam, G.: Adding open modules to AspectJ. In: Proceedings of the 5th International Conference on Aspect-Oriented Software Development (AOSD), March 2006, pp. 39–50 (2006)
Rajan, H., Leavens, G.T.: Ptolemy: A language with quantified, typed events. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 155–179. Springer, Heidelberg (2008)
Shaner, S.M., Leavens, G.T., Naumann, D.A.: Modular verification of higher-order methods with mandatory calls specified by model programs. In: International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), Montreal, Canada, October 2007, pp. 351–367. ACM Press, New York (2007)
Spivey, J.M.: Understanding Z: a Specification Language and its Formal Semantics. Cambridge University Press, New York (1988)
F. Steimann, T. Pawlitzki, S. Apel, C. Kästner. Types and modularity for implicit invocation with implicit announcement. ACM Trans. Softw. Eng. Methodol., 1:1–1:43 (2010)
Sullivan, K., Griswold, W.G., Rajan, H., Song, Y., Cai, Y., Shonle, M., TewariModular, N.: aspect-oriented design with xpis. ACM Trans. Softw. Eng. Methodol., 5:1–5:42 (September 2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Sánchez, J., Leavens, G.T. (2013). Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification. In: Binder, W., Bodden, E., Löwe, W. (eds) Software Composition. SC 2013. Lecture Notes in Computer Science, vol 8088. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39614-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-39614-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39613-7
Online ISBN: 978-3-642-39614-4
eBook Packages: Computer ScienceComputer Science (R0)