Patrick Lam
Viktor Kuncak
Martin Rinard
ABSTRACT
We present three aspect-oriented constructs (formats, scopes, and defaults) that, in combination with a specification language based on abstract sets of objects, enable the modular application of multiple arbitrarily precise (and therefore arbitrarily unscalable) analyses to scalably verify data structure consistency properties in sizable programs. Formats use a form of field introduction to group together the declarations of all of the fields that together comprise a given data structure. Scopes and defaults enable the developer to state certain data structure consistency properties once in a single specification construct that cuts across the preconditions and postconditions of the procedures in the system. Standard approaches, in contrast, scatter and duplicate such properties across the preconditions and postconditions. We have implemented a prototype implementation, specification, analysis, and verification system based on these constructs and used this system to successfully verify a range of data structure consistency properties in several programs.Most previous research in the field of aspect-oriented programming has focused on the use of aspect-oriented concepts in design and implementation. Our experience indicates that aspect-oriented concepts can also be extremely useful for specification, analysis, and verification.
- J. Aldrich. Open modules: Reconciling extensibility and information hiding. Software Engineering Properties of Languages for Aspect Technologies, March 2004.]]Google Scholar
- M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS 2004: International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices, March 2004.]] Google ScholarDigital Library
- D. Batory and S. O'Malley. The design and implementation of hierarchical software systems with reusable components. ACM Transactions on Software Engineering and Methodology, 1(4), Oct. 1992.]] Google ScholarDigital Library
- W. Blume and R. Eigenmann. Performance analysis of parallelizing compilers on the Perfect Benchmarks programs. IEEE Transactions on Parallel and Distributed Systems, 3(6):643--656, Nov. 1992.]] Google ScholarDigital Library
- L. Burdy, Y. Cheon, D. Cok, M. D. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. Technical Report NII-R0309, Computing Science Institute, Univ. of Nijmegen, March 2003.]]Google Scholar
- D. R. Cheriton and M. E. Wolf. Extensions for multi-module records in conventional programming languages. In Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 296--306. ACM Press, 1987.]] Google ScholarDigital Library
- M. C. Chu-Carroll. Supporting distributed collaboration through multidimensional software configuration management. In Proceedings of the 10th ICSE Workshop on Software Configuration Management, 2001.]] Google ScholarDigital Library
- C. Clifton and G. Leavens. Observers and assistants: A proposal for modular aspect-oriented reasoning. Technical Report TR 02-04, Department of Computer Science, Iowa State University, Mar. 2002.]]Google Scholar
- K. Fisler and S. Krishnamurthi. Modular verification of collaboration-based software designs. In Proceedings of the Joint European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, Vienna, Austria, Sept. 2001.]] Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lilibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended Static Checking for Java. In Proc. ACM PLDI, 2002.]] Google ScholarDigital Library
- E. Gamma, R. Helm, R. Johnson, and J. Vlisside. Design Patterns. Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading, Mass., 1994.]] Google ScholarDigital Library
- D. Janzen and K. D. Volder. Programming with crosscutting effective views. In M. Odersky, editor, 18th ECOOP, pages 195--218, 2004.]]Google Scholar
- G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. Griswold. An overview of AspectJ. In ECOOP, 2001.]] Google ScholarDigital Library
- G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J. Loingtier, and J. Irwin. Aspect-oriented programming. In ECOOP, 1997.]]Google ScholarCross Ref
- N. Klarlund, A. Møller, and M. I. Schwartzbach. MONA implementation secrets. In Proc. 5th International Conference on Implementation and Application of Automata. LNCS, 2000.]] Google ScholarDigital Library
- R. Laddad. AspectJ in Action. Manning Publications Company, Greenwich, CT, 2003.]]Google Scholar
- P. Lam, V. Kuncak, and M. Rinard. On modular pluggable analyses using set interfaces. Technical Report 933, MIT CSAIL, December 2003.]]Google Scholar
- P. Lam, V. Kuncak, and M. Rinard. On our experience with modular pluggable analyses. Technical Report 965, MIT CSAIL, September 2004.]]Google Scholar
- P. Lam, V. Kuncak, and M. Rinard. Generalized typestate checking for data structure consistency. In 6th International Conference on Verification, Model Checking and Abstract Interpretation, 2005.]] Google ScholarDigital Library
- P. Lam, V. Kuncak, and M. Rinard. Hob: A tool for verifying data structure consistency. In 14th International Conference on Compiler Construction (tool demo), April 2005.]] Google ScholarDigital Library
- P. Lam, V. Kuncak, K. Zee, and M. Rinard. The Hob project web page. http://catfish.csail.mit.edu/~plam/hob/, 2004.]]Google Scholar
- K. Lieberherr, D. Lorenz, and M. Mezini. Programming with aspectual components. Technical Report NU-CCS-99-01, College of Computer Science, Northeastern University, Mar. 1999.]]Google Scholar
- B. Liskov and J. Guttag. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2000.]] Google ScholarDigital Library
- A. Møller and M. I. Schwartzbach. The Pointer Assertion Logic Engine. In Proc. ACM PLDI, 2001.]] Google ScholarDigital Library
- D. Moon. Object-oriented programming with flavors. In OOPSLA, 1986.]] Google ScholarDigital Library
- H. Ossher and P. Tarr. Multi-dimensional separation of concerns using hyperspaces. Technical Report Research Report 21452, IBM, 1999.]]Google Scholar
- H. Ossher and P. Tarr. Using multidimensional separation of concerns to (re)shape evolving software. Communications of the ACM, Oct. 2001.]] Google ScholarDigital Library
- A. Popovici, T. Gross, and G. Alonso. Dynamic weaving for aspect-oriented programming. In Proceedings of the 1st International Conference on Aspect-Oriented Software Development, pages 141--147, Enschede, The Netherlands, 2002.]] Google ScholarDigital Library
- R. Reiter. A logic for default reasoning. Artificial Intelligence, pages 81--132, 1980.]]Google Scholar
- M. Rinard, A. Sǎlcianu, and S. Bugrara. A classification system and analysis for aspect-oriented programs. In Proc. 12th Symposium on the Foundations of Software Engineering, 2004.]] Google ScholarDigital Library
- M. C. Rinard. The Design, Implementation and Evaluation of Jade, a Portable, Implicitly Parallel Programming Language. PhD thesis, Stanford University, 1994.]] Google ScholarDigital Library
- A. Silberschatz and Z. Kedem. Consistency in hierarchical database systems. Journal of the ACM, 27(1):72--80, January 1980.]] Google ScholarDigital Library
- G. Snelting and F. Tip. Semantics-based composition of class hierarchies. In ECOOP, 2002.]] Google ScholarDigital Library
- M. Störzer and J. Krinke. Interference analysis for AspectJ. In Workshop on Foundations of Aspect-Oriented Languages, Mar. 2003.]]Google Scholar
- P. L. Tarr, H. Ossher, W. H. Harrison, and S. M. S. Jr. N degrees of separation: Multi-dimensional separation of concerns. In ICSE, 1999.]] Google ScholarDigital Library
- M. Wand, G. Kiczales, and C. Dutchyn. A semantics for advice and dynamic join points in aspect-oriented programming. Transactions on Programming Languages and Systems, 26(5), 2004.]] Google ScholarDigital Library
- K. Zee, P. Lam, V. Kuncak, and M. Rinard. Combining theorem proving with static analysis for data structure consistency. In International Workshop on Software Verification and Validation (SVV 2004), Seattle, November 2004.]]Google Scholar
Recommendations
Refactoring of Crosscutting Concerns with Metaphor-Based Heuristics
It has been advocated that Aspect-Oriented Programming (AOP) is an effective technique to improve software maintainability through explicit support for modularising crosscutting concerns. However, in order to take the advantages of AOP, there is a need ...
An implementation substrate for languages composing modularized crosscutting concerns
SAC '09: Proceedings of the 2009 ACM symposium on Applied ComputingWe present the implementation of several programming languages with support for multi-dimensional separation of concerns (MDSOC) on top of a common delegation-based substrate, which is a prototype for a dedicated MDSOC virtual machine. The supported ...
An Aspect-Oriented Approach for Assertion Verification
VALID '09: Proceedings of the 2009 First International Conference on Advances in System Testing and Validation LifecycleAssertions or formal program specifications are fundamental to build more reliable software. One of the most important applications of assertions is found in the Design by Contract metaphor: pre-conditions, invariants and post-conditions. Current ...
Comments