Client-aware checking and information hiding in interface specifications with JML/ajmlc

ABSTRACT

Information hiding controls which parts of a module are visible to different clients. This aids maintenance because hidden implementation details can be changed without affecting clients. The benefits of information hiding apply not only to code but also to other artifacts, such as specifications. In this demonstration we show how our client-aware checking (CAC) technique, which is implemented by our JML/ajmlc compiler and freely available online, use the privacy information in specifications to promote information hiding. We demonstrate the benefits of CAC over existing runtime assertion checkers (RACs) of contemporary interface specification languages.

Client-aware checking allows runtime assertion checking and error reporting based solely on specifications visible to clients. This avoids exposing hidden implementation or specification details that cannot be understood by non-privileged clients.

This demonstration will proceed by discussing the goals of the CAC technique by means of realistic examples. Attendees will mainly see JML specifications, including pre- and postconditions for methods. They will learn how to use the JML/ajmlc compiler, which also provides information hiding capabilities. In addition, they will learn how to use model fields to hide the actual field declarations in classes, and how model fields play an important role in achieving information hiding. We will conclude with pointers to ongoing work on design, implementation and runtime checking of Java programs with CAC-based JML/ajmlc.

References

1. M. Barnett and K. R. M. Leino. Weakest-precondition of unstructured programs. SIGSOFT Softw. Eng. Notes, 31:82--87, September 2005.
2. M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: an overview. In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, editors, Post Conference Proceedings of CASSIS: Construction and Analysis of Safe, Secure and Interoperable Smart devices, Marseille, volume 3362 of LNCS. Springer-Verlag, 2005.
3. K. K. Dhara and G. T. Leavens. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pages 258--267. IEEE Computer Society Press, Mar. 1996. A corrected version is ISU CS TR #95-20c, http://tinyurl.com/s2krg.
4. M. Fahndrich, M. Barnett, and F. Logozzo. Embedded contract languages. In Proceedings of the 2010 ACM Symposium on Applied Computing, SAC '10. ACM, 2010.
5. R. B. Findler and M. Felleisen. Contract soundness for object-oriented languages. In Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA '01, pages 1--15, New York, NY, USA, 2001. ACM.
6. G. Kiczales. Beyond the black box: Open implementation. IEEE Softw., 13(1):8--11, Jan. 1996.
7. G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 2006.
8. G. T. Leavens and P. Müller. Information hiding and visibility in interface specifications. In International Conference on Software Engineering (ICSE), pages 385--395. IEEE, May 2007.
9. B. Meyer. Eiffel: the language. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1992.
10. B. Meyer. Object-oriented software construction (2nd ed.). Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1997.
11. D. L. Parnas. On the criteria to be used in decomposing systems into modules. Commun. ACM, 15:1053--1058, December 1972.
12. H. Rebelo, R. Lima, G. T. Leavens, M. Cornelio, A. Mota, and C. Oliveira. Optimizing generated aspect-oriented assertion checking code for jml using program transformations: An empirical study. Science of Computer Programming, 78(8):1137--1156, 2013.
13. H. Rebelo, S. Soares, R. Lima, L. Ferreira, and M. Cornelio. Implementing Java modeling language contracts with AspectJ. In Proceedings of the 2008 ACM symposium on Applied computing, SAC '08, pages 228--233, New York, NY, USA, 2008. ACM.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Reliability

    • Validation

• Software and its engineering

  • Software creation and management

    • Software verification and validation

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Assertions

      • Invariants

      • Pre- and post-conditions

      • Program specifications