Editing Class invariant (section)

====Java====
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.

<syntaxhighlight lang="Java">public class Date {
    int /*@spec_public@*/ day;
    int /*@spec_public@*/ hour;

    /*@invariant day >= 1 && day <= 31; @*/ //class invariant
    /*@invariant hour >= 0 && hour <= 23; @*/ //class invariant

    /*@
    @requires d >= 1 && d <= 31;
    @requires h >= 0 && h <= 23;
    @*/
    public Date(int d, int h) { // constructor
        day = d;
        hour = h;
    }

    /*@
    @requires d >= 1 && d <= 31;
    @ensures day == d;
    @*/
    public void setDay(int d) {
        day = d;
    }

    /*@
    @requires h >= 0 && h <= 23;
    @ensures hour == h;
    @*/
    public void setHour(int h) {
        hour = h;
    }
}</syntaxhighlight>