Class Invariants

Class invariants are a concept which allow you to assure that your target class is always in a valid ("invariant") state. They can be used to restrain the value of class variables to a certain range (being never null, or a collection to hold at least 1 object, ...).

To define a class invariant, you have to implement a method called classInvariant() in your contract:

public class DummyContract {
  
    public void classInvariant() {
        // check some properties of the target class
        ...
    }
	
}

Everytime a method of the target class (or subtypes of it) gets called, the classInvariant() method is called afterwards.

In order to see a full example of a class invariant, click here.