Abstract
We define bisimilarity for an aspect extension of the untyped lambda calculus and prove that it is sound and complete for contextual reasoning about programs. The language we study is very small, yet powerful enough to encode mutable references and a range of temporal pointcuts. We extend formal studies of Open Modules to this more general setting. Examples suggest that aspects are amenable to techniques developed for stateful higher-order programs. To our knowledge, this is the first study of coinductive reasoning principles for aspect programs.
Based on an extended abstract published in AOSD 07, March 12–16, 2007, Vancouver, Canada, 1-59593-615-7/07/03.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aksit, M., Wakita, K., Bosch, J., Bergmans, L., Yonezawa, A.: Abstracting object-interactions using composition-filters. In: Object-based distributed processing. LNCS (1993)
Bergmans, L.: Composing Concurrent Objects - Applying Composition Filters for the Development and Reuse of Concurrent Object-Oriented Programs. Ph.D. thesis, University of Twente (1994)
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–355. Springer, Heidelberg (2001)
Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C.V., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997)
Lieberherr, K.J.: Adaptive Object-Oriented Software: The Demeter method with propagation patterns. PWS Publishing Company (1996)
Ossher, H., Tarr, P.: Multi-dimensional separation of concerns and the hyperspace approach. In: Proceedings of the Symposium on Software Architectures and Component Technology: The State of the Art in Software Development (2001)
Filman, R., Friedman, D.: Aspect-oriented programming is quantification and obliviousness. In: Workshop on Advanced Separation of Concerns (2000)
Tarr, P.L., Ossher, H.: Hyper/J: Multi-dimensional separation of concerns for Java. In: ICSE, pp. 729–730 (2001)
Coady, Y., Kiczales, G., Feeley, M.J., Smolyn, G.: Using AspectC to improve the modularity of path-specific customization in operating system code. In: ESEC/SIGSOFT FSE, pp. 88–98 (2001)
Dutchyn, C., Tucker, D.B., Krishnamurthi, S.: Semantics and scoping of aspects in higher-order languages. Sci. Comput. Program. 63(3), 207–239 (2006)
Walker, D., Zdancewic, S., Ligatti, J.: A theory of aspects. In: Runciman, C., Shivers, O. (eds.) ICFP, pp. 127–139. ACM, New York (2003)
Sangiorgi, D.: Bisimulation: From the origins to today. In: LICS, pp. 298–302. IEEE Computer Society, Los Alamitos (2004)
Sangiorgi, D.: The bisimulation proof method: Enhancements and open problems. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 18–19. Springer, Heidelberg (2006)
Gordon, A.D.: Operational equivalences for untyped and polymorphic object calculi. In: Gordon, A.D., Pitts, A.M. (eds.) Higher-Order Operational Techniques in Semantics, Publications of the Newton Institute, pp. 9–54. Cambridge University Press, Cambridge (1998)
Pitts, A.M.: Operationally-based theories of program equivalence. In: Dybjer, P., Pitts, A.M. (eds.) Semantics and Logics of Computation, Publications of the Newton Institute, pp. 241–298. Cambridge University Press, Cambridge (1997)
Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. J. ACM 54(5) (2007)
Jeffrey, A., Rathke, J.: A theory of bisimulation for a fragment of concurrent ML with local names. Theor. Comput. Sci. 323(1-3), 1–48 (1999); Preliminary version appeared in IEEE LICS 1999
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Morrisett and Jones [50], pp. 141–152
Gordon, A.D., Rees, G.D.: Bisimilarity for a first-order calculus of objects with subtyping. In: POPL, pp. 386–395 (1996)
Koutavas, V., Wand, M.: Bisimulations for untyped imperative objects. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 146–161. Springer, Heidelberg (2006)
Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables. In: POPL, pp. 191–203 (1988)
Kiczales, G., Mezini, M.: Aspect-oriented programming and modular reasoning. In: ICSE 2005: Proceedings of the 27th international conference on software engineering, pp. 49–58. ACM Press, New York (2005)
Aldrich, J.: Open modules: Modular reasoning about advice. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 144–168. Springer, Heidelberg (2005)
Ongkingco, N., Avgustinov, P., Tibble, J., Hendren, L., de Moor, O., Sittampalam, G.: Adding open modules to AspectJ. In: AOSD 2006: Proceedings of the 5th international conference on Aspect-oriented software development, pp. 39–50. ACM Press, New York (2006)
Avgustinov, P., Bodden, E., Hajiyev, E., Hendren, L., Lhoták, O., de Moor, O., Ongkingco, N., Sereni, D., Sittampalam, G., Tibble, J.: Aspects for trace monitoring. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 20–39. Springer, Heidelberg (2006)
Alur, R.: The benefits of exposing calls and returns. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 2–3. Springer, Heidelberg (2005)
Alur, R., Madhusudan, P.: Adding nesting structure to words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 1–13. Springer, Heidelberg (2006)
Clifton, C., Leavens, G.T.: MiniMAO: An imperative core language for studying aspect-oriented reasoning. Sci. Comput. Program. 63(3), 321–374 (2006)
Jagadeesan, R., Jeffrey, A., Riely, J.: An untyped calculus of aspect oriented programs. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, Springer, Heidelberg (2003)
Clifton, C., Leavens, G.T., Wand, M.: Parameterized aspect calculus: A core calculus for the direct study of aspect-oriented languages (2003), http://www.cs.iastate.edu/~cclifton/papers/TR03-13.pdf
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Rajan, H., Sullivan, K.J.: Classpects: unifying aspect- and object-oriented language design. In: Roman, G.-C., Griswold, W.G., Nuseibeh, B. (eds.) ICSE, pp. 59–68. ACM, New York (2005)
Wand, M., Kiczales, G., Dutchyn, C.: A semantics for advice and dynamic join points in aspect-oriented programming. TOPLAS 26(5), 890–910 (2004)
Masuhara, H., Kiczales, G., Dutchyn, C.: A compilation and optimization model for aspect-oriented programs. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 46–60. Springer, Heidelberg (2003)
Ligatti, J., Walker, D., Zdancewic, S.: A type-theoretic interpretation of pointcuts and advice. Sci. Comput. Program. 63(3), 240–266 (2006)
Jagadeesan, R., Jeffrey, A., Riely, J.: Typed parametric polymorphism for aspects. Sci. Comput. Program. 63(3), 267–296 (2006)
Li, H.C., Krishnamurthi, S., Fisler, K.: Modular verification of open features using three-valued model checking. Autom. Softw. Eng. 12(3), 349–382 (2005)
Sihman, M., Katz, S.: Model checking applications of aspects and superimpositions. In: Foundations of Aspect Languages (2003)
Ubayashi, N., Tamai, T.: Aspect-oriented programming with model checking. In: AOSD 2002: Proceedings of the 1st international conference on Aspect-oriented software development, pp. 148–154. ACM Press, New York (2002)
Dantas, D.S., Walker, D.: Harmless advice. In: Morrisett and Jones [50], pp. 383–396
Nakajima, S., Tamai, T.: Lightweight formal analysis of aspect-oriented models. In: UML 2004 Workshop on Aspect-Oriented Modeling (2004)
Abramsky, S., Ong, C.-H.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993)
Gordon, A.D.: Bisimilarity as a theory of functional programming. Electr. Notes Theor. Comput. Sci. 1 (1995)
Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103–112 (1996)
Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. Theor. Comput. Sci. 375(1-3), 169–192 (2007)
Koutavas, V., Wand, M.: Proving class equivalence (submitted for publication) (July 2006)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: LICS, pp. 293–302. IEEE Computer Society, Los Alamitos (2007)
Sangiorgi, D.: A theory of bisimulation for the pi-calculus. Acta Inf. 33(1), 69–97 (1996)
Lassen, S.: Eager normal form bisimulation. In: LICS, pp. 345–354. IEEE Computer Society Press, Los Alamitos (2005)
Lassen, S.B.: Head normal form bisimulation for pairs and the λμ-calculus. In: LICS, pp. 297–306. IEEE Computer Society Press, Los Alamitos (2006)
Støvring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 161–172. ACM, New York (2007)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)
Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)
Lassen, S.B., Levy, P.B.: Typed normal form bisimulation. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 283–297. Springer, Heidelberg (2007)
Bockisch, C., Haupt, M., Mezini, M., Ostermann, K.: Virtual machine support for dynamic join points. In: AOSD, pp. 83–92 (2004)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Gordon, A.D.: A tutorial on co-induction and functional programming. In: Glasgow functional programming workshop, pp. 78–95. Springer, Heidelberg (1994)
Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)
Felleisen, M., Friedman, D.P., Kohlbecker, E., Duba, B.: A syntactic theory of sequential control. Theor. Comput. Sci. 52(3), 205–237 (1987)
De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34(1-2), 83–133 (1984)
Jeffrey, A., Rathke, J.: Java Jr: Fully abstract trace semantics for a core Java language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423–438. Springer, Heidelberg (2005)
Morris, J.H.: Lambda-Calculus Models of Programming Languages. PhD thesis, MIT (December 1968)
Abadi, M., Fournet, C.: Access control based on execution history. In: Proceedings of the Network and Distributed System Security Symposium Conference (2003)
Boebert, W.E., Kain, R.Y.: A practical alternative to hierarchical integrity policies. In: Proceedings of the Eighth National Computer Security Conference (1985)
Walker, K.M., Sterne, D.F., Badger, M.L., Petkac, M.J., Shermann, D.L., Oostendorp, K.A.: Confining root programs with Domain and Type Enforcement (DTE). In: Proceedings of the Sixth USENIX UNIX Security Symposium (1996)
Loscocco, P.A., Smalley, S.D.: Meeting critical security objectives with Security-Enhanced Linux. In: Proceedings of the 2001 Ottawa Linux Symposium (2001)
Sangiorgi, D.: Expressing Mobility in Process Algebras: First Order and Higher Order Paradigms. PhD thesis, University of Edinburgh (1993)
Milner, R.: Communication and concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)
Landin, P.J.: The mechanical evaluation of expressions. Computer Journal 6(4), 308–320 (1964)
Morrisett, J.G., Jones, S.L.P. (eds.): Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Jagadeesan, R., Pitcher, C., Riely, J. (2009). Open Bisimulation for Aspects. In: Rashid, A., Ossher, H. (eds) Transactions on Aspect-Oriented Software Development V. Lecture Notes in Computer Science, vol 5490. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02059-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-02059-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02058-2
Online ISBN: 978-3-642-02059-9
eBook Packages: Computer ScienceComputer Science (R0)