What is a class invariant?

ABSTRACT

This paper is a progress report on our research into the problem of automatically identifying and using class invariants in object-oriented programs. We introduce an example of a class invariant in Java, and review applications for class invariants in software engineering tools and in compiler optimization. We then focus on an elementary problem of definition: what is a class invariant? This question gives an interesting perspective on programming language design. We conclude that there are many reasonable categories of class invariants, and that the problem of finding good definitions cannot be solved by a thought experiment. The only way to choose good categories is to experiment with the analysis of real programs, to see which categories of class invariant are actually useful. Our current research focuses on these experiments.

REFERENCES

• 1: L. Boynton and J. Payne. Java class java.util.vector, Dec. 1997. Version 1.38, Sun Microsystems Inc.
• 2: Program modularity and scaling of program analysis: position statement. Report of the Dagstuhl Seminar on Program Analysis (Dagstuhl Seminar 236), 1999.
• 3: D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Compaq SRC Resarch Report 159, 1998.
• 4: Bart Jacobs , Joachim van den Berg , Marieke Huisman , Martijn van Berkum , U. Hensel , H. Tews, Reasoning about Java classes: preliminary report, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.329-340, October 18-22, 1998, Vancouver, British Columbia, Canada
• 5: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML.Technical Report 98-060, Iowa State University, May 2001.
• 6: David C. Luckham, Programming with Specifications: An Introduction to Anna, a Language for Specifying ADA Programs, Springer-Verlag New York, Inc., Secaucus, NJ, 1990
• 7: B. Meyer. The importance of the class invariant. At http://www.elj.com/eiffel/bm/invariants.
• 8: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 9: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 10: David E. Monarchi , Gretchen I. Puhr, A research typology for object-oriented analysis and design, Communications of the ACM, v.35 n.9, p.35-47, Sept. 1992 [doi>10.1145/130994.130995]
• 11: Jean-Marc Nerson, Applying object-oriented analysis and design, Communications of the ACM, v.35 n.9, p.63-74, Sept. 1992 [doi>10.1145/130994.130997]
• 12: J. van den Berg, C.-B. Breunesse, B. Jacobs, and E. Poll. On the role of invariants in reasoning about object-oriented languages. To appear in: Workshop on Formal Techniques for Java Programs, ECOOP 2001, Budapest, Hungary, June 18, 2001.
• 13: Adam Brooks Webber, Program analysis using binary relations, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.249-260, June 16-18, 1997, Las Vegas, Nevada, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Object-oriented constructs

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Java

General Terms:
Algorithms, Languages