Open bisimulation for aspects

ABSTRACT

We define and study bisimulation for proving contextual equivalence in an aspect extension of the untyped lambda-calculus. To our knowledge, this is the first study of coinductive reasoning principles aimed at proving equality of aspect programs. The language we study is very small, yet powerful enough to encode mutable references and a range of temporal pointcuts (including cflow and regular event patterns).Examples suggest that our bisimulation principle is useful. For an encoding of higher-order programs with state, our methods suffice to establish well-known and well-studied subtle examples involving higher-order functions with state.Even in the presence of first class dynamic advice and expressive pointcuts, our reasoning principles show that aspect-aware interfaces can aid in ensuring that clients of a component are unaffected by changes to an implementation. Our paper generalizes existing results given for open modules to also include a variety of history-sensitive pointcuts such as cflow and regular event patterns.Our formal techniques and results suggest that aspects are amenable to the formal techniques developed for stateful higher-order programs.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: M. Abadi and C. Fournet. Access control based on execution history. In Proceedings of the Network and Distributed System Security Symposium Conference, 2003.
• 3: Samson Abramsky , Radha Jagadeesan , Pasquale Malacaria, Full abstraction for PCF, Information and Computation, v.163 n.2, p.409-470, Dec 2000 [doi>10.1006/inco.2000.2930]
• 4: Samson Abramsky , C.-H. Luke Ong, Full abstraction in the lazy lambda calculus, Information and Computation, v.105 n.2, p.159-267, Aug. 1993 [doi>10.1006/inco.1993.1044]
• 5: Mehmet Aksit , Ken Wakita , Jan Bosch , Lodewijk Bergmans , Akinori Yonezawa, Abstracting Object Interactions Using Composition Filters, Proceedings of the Workshop on Object-Based Distributed Programming, p.152-184, July 26-27, 1993
• 6: J. Aldrich. Open modules: Modular reasoning about advice. In A. P. Black, editor, ECOOP, volume 3586 of Lecture Notes in Computer Science, pages 144--168. Springer, 2005.
• 7: Rajeev Alur, The benefits of exposing calls and returns, Lecture Notes in Computer Science, Springer-Verlag, London, 2005 [doi>10.1007/11539452_2]
• 8: R. Alur and P. Madhusudan. Adding nesting structure to words. In O. H. Ibarra and Z. Dang, editors, Developments in Language Theory, volume 4036 of Lecture Notes in Computer Science, pages 1--13. Springer, 2006.
• 9: P. Avgustinov, E. Bodden, E. Hajiyev, L. Hendren, O. Lhoták, O. de Moor, N. Ongkingco, D. Sereni, G. Sittampalam, and J. Tibbie. Aspects for trace monitoring. In K. Havelund, M. Nunez, G. Rosu, and B. Wolff, editors, Formal Approaches to Testing Systems and Runtime Verification (FATES/RV), Lecture Notes in Computer Science. Springer, 2006.
• 10: L. Bergmans. Composing Concurrent Objects - Applying Composition Filters for the Development and Reuse of Concurrent Object-Oriented Programs. Ph.D. thesis, University of Twente, 1994.
• 11: Christoph Bockisch , Michael Haupt , Mira Mezini , Klaus Ostermann, Virtual machine support for dynamic join points, Proceedings of the 3rd international conference on Aspect-oriented software development, p.83-92, March 22-24, 2004, Lancaster, UK [doi>10.1145/976270.976282]
• 12: W. E. Boebert and R. Y. Kain. A practical alternative to hierarchical integrity policies. In Proceedings of the Eighth National Computer Security Conference, 1985.
• 13: C. Clifton and G. T. Leavens. MiniMAO1: An imperative core language for studying aspect-oriented reasoning. Science of Computer Programming, 2006. To appear.
• 14: C. Clifton, G. T. Leavens, and M. Wand. Parameterized aspect calculus: A core calculus for the direct study of aspect-oriented languages. At http://www.cs.iastate.edu/~cclifton/papers/TR03--13.pdf, 2003.
• 15: Yvonne Coady , Gregor Kiczales , Mike Feeley , Greg Smolyn, Using aspectC to improve the modularity of path-specific customization in operating system code, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 16: D. S. Dantas and D. Walker. Harmless advice. In Morrisett and Jones {47}, pages 383--396.
• 17: R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34(1--2):83--133, Nov. 1984.
• 18: David B. Tucker , Shriram Krishnamurthi, Pointcuts and advice in higher-order languages, Proceedings of the 2nd international conference on Aspect-oriented software development, p.158-167, March 17-21, 2003, Boston, Massachusetts [doi>10.1145/643603.643620]
• 19: M. Felleisen , D. P. Friedman , E. Kohlbecker , B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, v.52 n.3, p.205-237, June 1987 [doi>10.1016/0304-3975(87)90109-5]
• 20: R. Filman and D. Friedman. Aspect-oriented programming is quantification and obliviousness. In Workshop on Advanced Separation of Concerns, 2000.
• 21: A. D. Gordon. Bisimilarity as a theory of functional programming. Electr. Notes Theor. Comput. Sci., 1, 1995.
• 22: A. D. Gordon, Operational equivalences for untyped and polymorphic object calculi, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 23: Andrew D. Gordon , Gareth D. Rees, Bisimilarity for a first-order calculus of objects with subtyping, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.386-395, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237807]
• 24: Douglas J. Howe, Proving congruence of bisimulation in functional programming languages, Information and Computation, v.124 n.2, p.103-112, Feb. 1, 1996 [doi>10.1006/inco.1996.0008]
• 25: J. M. E. Hyland , C.-H. L. Ong, On full abstraction for PCF: I, II, and III, Information and Computation, v.163 n.2, p.285-408, Dec 2000 [doi>10.1006/inco.2000.2917]
• 26: R. Jagadeesan, A. Jeffrey, and J. Riely. An untyped calculus of aspect oriented programs. In Conference Record of ECOOP 03: The European Conference on Object-Oriented Programming, volume 2743 of Lecture Notes in Computer Science, 2003.
• 27: R. Jagadeesan, A. Jeffrey, and J. Riely. Typed parametric polymorphism for aspects. Science of Computer Programming, 2006. To appear.
• 28: R. Jagadeesan, C. Pitcher, and J. Riely. Open bisimulation for aspects (full version). Available at http://www.teasp.org/bisimulation, 2007.
• 29: Alan Jeffrey , Julian Rathke, A theory of bisimulation for a fragment of concurrent ML with local names, Theoretical Computer Science, v.323 n.1-3, p.1-48, 14 September 2004 [doi>10.1016/j.tcs.2004.03.005]
• 30: A. Jeffrey and J. Rathke. Java Jr: Fully abstract trace semantics for a core Java language. In ESOP, volume 3444 of LNCS, pages 423--438. Springer, 2005.
• 31: Gregor Kiczales , Erik Hilsdale , Jim Hugunin , Mik Kersten , Jeffrey Palm , William G. Griswold, An Overview of AspectJ, Proceedings of the 15th European Conference on Object-Oriented Programming, p.327-353, June 18-22, 2001
• 32: G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. V. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming. In European Conference on Object-Oriented Programming (ECOOP), 1997.
• 33: Gregor Kiczales , Mira Mezini, Aspect-oriented programming and modular reasoning, Proceedings of the 27th international conference on Software engineering, p.49-58, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062482]
• 34: V. Koutavas and M. Wand. Bisimulations for untyped imperative objects. In P. Sestoft, editor, Proc. ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 146--161. Springer, Mar. 2006.
• 35: V. Koutavas and M. Wand. Proving class equivalence, submitted for publication, July 2006.
• 36: V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In Morrisett and Jones {47}, pages 141--152
• 37: P. J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4):308--320, Jan. 1964.
• 38: Soren Lassen, Eager Normal Form Bisimulation, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), p.345-354, June 26-29, 2005 [doi>10.1109/LICS.2005.15]
• 39: Soren B. Lassen, Head Normal Form Bisimulation for Pairs and the \lambda\mu-Calculus, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.297-306, August 12-15, 2006 [doi>10.1109/LICS.2006.29]
• 40: Harry C. Li , Shriram Krishnamurthi , Kathi Fisler, Modular Verification of Open Features Using Three-Valued Model Checking, Automated Software Engineering, v.12 n.3, p.349-382, July 2005 [doi>10.1007/s10515-005-2643-9]
• 41: Karl J. Lieberherr, Adaptive Object-Oriented Software: The Demeter Method with Propagation Patterns, PWS Publishing Co., Boston, MA, 1995
• 42: J. Ligatti, D. Walker, and S. Zdancewic. A type-theoretic interpretation of pointcuts and advice. Science of Computer Programming, 2006. To appear.
• 43: P. A. Loscocco and S. D. Smalley. Meeting critical security objectives with Security-Enhanced Linux. In Proceedings of the 2001 Ottawa Linux Symposium, 2001.
• 44: H. Masuhara, G. Kiczales, and C. Dutchyn. A compilation and optimization model for aspect-oriented programs. In G. Hedin, editor, CC, volume 2622 of Lecture Notes in Computer Science, pages 46--60. Springer, 2003.
• 45: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 46: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 47: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 2006
• 48: S. Nakajima and T. Tamai. Lightweight formal analysis of aspect-oriented models. In UML2004 Workshop on Aspect-Oriented Modeling, 2004.
• 49: Neil Ongkingco , Pavel Avgustinov , Julian Tibble , Laurie Hendren , Oege de Moor , Ganesh Sittampalam, Adding open modules to AspectJ, Proceedings of the 5th international conference on Aspect-oriented software development, March 20-24, 2006, Bonn, Germany [doi>10.1145/1119655.1119664]
• 50: H. Ossher and P. Tarr. 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.
• 51: A. M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation, Publications of the Newton Institute, pages 241--298. Cambridge University Press, 1997.
• 52: Hridesh Rajan , Kevin J. Sullivan, Classpects: unifying aspect- and object-oriented language design, Proceedings of the 27th international conference on Software engineering, p.59-68, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062483]
• 53: D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST-99-93, Department of Computer Science, University of Edinburgh, 1992.
• 54: D. Sangiorgi. Expressing Mobility in Process Algebras: First Order and Higher Order Paradigms. PhD thesis, University of Edinburgh, 1993.
• 55: Davide Sangiorgi, A theory of bisimulation for the &lgr;-calculus, Acta Informatica, v.33 n.1, p.69-97, 1996 [doi>10.1007/s002360050036]
• 56: Davide Sangiorgi, Bisimulation: From The Origins to Today, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.298-302, July 13-17, 2004 [doi>10.1109/LICS.2004.13]
• 57: D. Sangiorgi. The bisimulation proof method: Enhancements and open problems. In R. Gorrieri and H. Wehrheim, editors, FMOODS, volume 4037 of Lecture Notes in Computer Science, pages 18--19. Springer, 2006.
• 58: M. Sihman and S. Katz. Model checking applications of aspects and superimpositions. In Foundations of Aspect Languages, 2003.
• 59: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.63-74, January 12-14, 2005, Long Beach, California, USA
• 60: Peri Tarr , Harold Ossher, Hyper/J: multi-dimensional separation of concerns for Java, Proceedings of the 23rd International Conference on Software Engineering, p.729-730, May 12-19, 2001, Toronto, Ontario, Canada
• 61: Naoyasu Ubayashi , Tetsuo Tamai, Aspect-oriented programming with model checking, Proceedings of the 1st international conference on Aspect-oriented software development, April 22-26, 2002, Enschede, The Netherlands [doi>10.1145/508386.508405]
• 62: David Walker , Steve Zdancewic , Jay Ligatti, A theory of aspects, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.127-139, August 25-29, 2003, Uppsala, Sweden
• 63: K. M. Walker, D. F. Sterne, M. L. Badger, M. J. Petkac, D. L. Shermann, and K. A. Oostendorp. Confining root programs with Domain and Type Enforcement (DTE). In Proceedings of the Sixth USENIX UNIX Security Symposium, 1996.
• 64: Mitchell Wand , Gregor Kiczales , Christopher Dutchyn, A semantics for advice and dynamic join points in aspect-oriented programming, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.5, p.890-910, September 2004 [doi>10.1145/1018203.1018208]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Languages

Keywords:
aspect-oriented programming, contextual equivalence, equational reasoning, modular reasoning, modularity, open bisimulation