3.4 Invariant of an object

There are certain general aspects of the specification which are so basic that they are part of the invariant included in the state schema of all objects; surrogate' = surrogate is an example. All operations in which this object participates must preserve the surrogate of the object. Other requirements are slightly less basic and are part of the invariant for most, but not all, operations. For instance, (name',context') = (name,context), unless the operation changes names, including the change of an identifier. In fact, the set of (name,context) pairs has to remain the same, unless names are changes/added/deleted. Note that it is useful to have special name-related operations in the toolkit. They would be used, for example, to correct a Social Security Number which has been entered incorrectly into some record.

The invariant of an object (as well as the invariant that defines a particular collection of objects, see below) may be considered as a conjunct of the global property. This approach is correct, but hardly helpful for large specifications: a better structuring seems to be essential for human understanding. For example, the notion of sections in [Uni95] provides a good indication of an approach to come in standard Z. In the absence of a syntactically-supported construct, we can only rely on conventions (such as invariant of an operation described, eg, in [ISO95c]) that help us to consider only the relevant fragments of a large specification. This may lead to redundancies (such as explicit inclusion of the relevant fragments of the object invariant in operation schemas) which are very helpful for human understanding.

Note that conjuncts of the template type are checked as a fragment of the precondition for creation or initialization of an object. Clearly the template type must be known. Each input value provided as a property value must satisfy the invariant of that value's type (ie domain - see [Kil89]). In addition, these values collectively must satisfy the invariant of the object. An object satisfying its template type obviously satisfies every conjunct of this type. Each of these conjuncts may be considered a supertype of the template type, e.g. - for a person - being a legal entity, having a name, etc. But what of optional types for which no information is known at initialization?