What is a class invariant?

摘要

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.