Class invariant
From Wikipedia, the free encyclopedia
- This article is about class invariants in computer programming, for use of the term in mathematics, see equivalence class and invariant.
In computer programming, a class invariant is an invariant used to constrain objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object.
Class invariants are established during construction and constantly maintained between calls to public methods. Temporary breaking of class invariance between private method calls is possible, although not encouraged.
An object invariant, or representation invariant, is a programming construct consisting of a set of invariant properties that remain uncompromised regardless of the state of the object. This ensures that the object will always meet predefined conditions, and that methods may, therefore, always reference the object without the risk of making inaccurate presumptions. Defining class invariant can help programmers and testers to catch more bugs during software testing.
Common programming languages like C++ and Java support assertions by default, which can be used to define class invariants. For Java, there is a more powerful tool called Java Modeling Language that provides a more robust way of defining class invariants.
[edit] Example
This is an example of a class invariant in the Java programming language with Java Modeling Language. The invariant must hold to be true after the constructor is finished and at the entry and exit of all public member functions. Public member functions should define precondition and postcondition to help ensure the class invariant.
public class Date { int /*@spec_public@*/ day; int /*@spec_public@*/ hour; /*@invariant 1<=day && day <=31; @*/ //class invariant /*@invariant 0<=hour && hour < 24; @*/ //class invariant /*@ @requires 1 <= d && d <=31; @requires 0<=h && h < 24; @*/ public Date(int d, int h){ day = d; hour = h; } //constructor /*@ @requires 1 <= d && d <=31; @ensures day == d; @*/ public void setDay(int d) { if(1 <= d && d <=31) day = d; } /*@ @requires 0<=h && h < 24; @ensures hour == h; @*/ public void setHour(int h) { if(0<=h && h < 24) hour = h; } }
