Invariant field

When creating an attribute, you can optionally enter or select an invariant for that feature. That invariant will be added to the end of the existing invariant clause. If the invariant clause did not exist before, it is now created.

If the attribute is of a reference type, you may select the invariant that the attribute may never be void. If it is of a basic expanded type, some other standard options may be chosen. For example, for INTEGER you may select that it should always be positive.

The example above will generate the code: invariant count_positive: count > 0