Go to the first, previous, next, last section, table of contents.


7.3 Class Invariants

The invariant-clause specifies an invariant property that must be true of all values of the type. More precisely, the specified property must be true of the abstract value of each assigned object of the type in all visible states. (This semantics is based on the work of Poetzsch-Heffter [Poetzsch-Heffter97].) The syntax is as follows.

invariant-clause ::= invariant [ redundantly ] predicate ;

In stating an invariant, one uses the state function \any. For example, one might write self\any to refer to the abstract value of an arbitrary object of the class being specified. More commonly, as in the invariant of the class Person repeated below (see section 7.1.1 A First Class Design (Person)), one applies \any to the specification variables of the class. This says that the abstract values of assigned Person objects must have a name field that is not empty, and with a age field that is nonnegative.

invariant len(name\any) > 0 /\ age\any >= 0;

One helpful way to think of a class invariant is as a restriction on the space of abstract values for that class. For example, the invariant for Person objects given above can be thought of as saying that the subset of abstract values of the sort Person that is of interest is the subset in which the name field is not empty and the age field is nonnegative. The way this restriction is accomplished is by asserting that the invariant property is true of all assigned objects in each visible state. (Note that self and data members are not required to be assigned in the pre-state for constructors.)

Both the pre- and post-states of a public member function are visible states, since they can be seen by clients. However, hidden states may exist during the execution of a member function, and in these states an invariant may be temporarily violated. This is okay, because clients of a class never see such intermediate states.

Because the pre- and post-states are visible, it may also help to manifest invariants of assigned objects as redundant pre- and postconditions for each member function. That is, one can assume the invariant as a redundant precondition, for each assigned object, with \any changed to \pre. If desired, the invariant can be highlighted in function specifications by the use of a redundant requires-clause (see section 6.9.2 Redundant Requires Clauses). Recall, however, that an object and its fields are not assigned upon entry to a constructor, so one would not assume the invariant in the precondition of a constructor.

Similarly, one can claim invariants for assigned objects as redundant postconditions, with \any changed to \post. If desired, these redundant predicates can be stated in a redundant ensures-clause. This shows that whenever a function is allowed to modify an assigned object, for example, self, a correct implementation must ensure that the invariant holds for each such object in the post-state.

Although invariants can manifest themselves as redundant requires-clauses and ensures-clauses in function specifications, the logical formulas used in the invariant do not have to be redundant with the rest of the specification of a class. That is, they can add information to a specification that might otherwise be absent.

Redundancy can also be used to help debug invariants. An invariant with the keyword redundantly does not affect the meaning of a specification, but is used to state some redundant property that should follow from the non-redundant invariants.

The formalization of this interpretation of invariants is that the invariant states a theory that is true of all assigned objects of the appropriate type in all visible states. An invariant involving data members of an object of a class is asserted to hold for those data members in all assigned objects of that class in all visible states [Poetzsch-Heffter97]. An invariant involving static or global variables is asserted to hold for those variables whenever they are assigned in visible states.

The semantics requires the invariant to hold in all visible states substituted for any, for each such assigned object mentioned in the invariant.(6)

What happens if the specification of a function is written in such a way that it seems that a correct implementation would violate the invariant? Then the function becomes overconstrained, and cannot be correctly implemented, since a correct implementation would have to both satisfy and violate the invariant.

As an example, consider the following function specification, which might be a member in the class Person. We highlight the relevant parts of the invariant by stating redundant pre- and postconditions.

// @(#)$Id: bad_myo.lh,v 1.4 1998/08/27 22:56:48 leavens Exp $

#include "Person.lh"

void Person::Make_Year_Older() throw();
//@ behavior {
//@   requires redundantly assigned(age,pre) /\ visible(pre) /\ age^ >= 0;
//@   modifies age;
//@   ensures age' = -3;   // wrong!
//@   ensures redundantly assigned(age,post) /\ visible(post) /\ age' >= 0;
//@ }

The problem is clearly seen by comparing the postcondition and the claimed redundant postcondition. It's clear that the post-state cannot make age' both equal to -3 and also nonnegative.

To formalize this idea, we first rewrite the use of data members in invariants to make them refer to these data members through self. This rewriting takes advantage of the automatically-generated trait constructed for a class by Larch/C++, which treats specification variables as objects that are part of a tuple that makes up the abstract value of self. (See section 7.1.1 A First Class Design (Person) for the trait Person_Trait.) For example, we can rewrite the invariant for Person as follows.

invariant len(self\any.name\any) > 0 /\ self\any.age\any >= 0;

Once this is done, we have an invariant-clause of the form invariant invariant_pred(self, any); this can be thought of as translated into the use of two traits. The uses-clause, exemplified by the one given below, would appear outside any class declaration in which the invariant-clause appears. The first trait used is always Invariant(T), where the sort of self is Obj[T]. The second trait, written as ITranslation below, would be different each time; it would be generated for each invariant clause as described below.

//@ uses Invariant(T), ITranslation;

The trait Invariant is the following, which just includes two other traits.

% @(#)$Id: Invariant.lsl,v 1.1 1997/01/27 20:33:15 leavens Exp $
Invariant(T): trait
  includes Invariant_Visible(Obj, T),
           Invariant_Visible(ConstObj, T)

The trait Invariant_Visible that is included by the above is the following. This trait states that every assigned object in a visible state satisfies the invariant predicate, invariant_pred. By including this trait for both regular and constant objects, all assigned objects of the class are covered. (See section 2.8.1 Formal Model of Objects for the trait TypedObj.)

% @(#)$Id: Invariant_Visible.lsl,v 1.1 1997/01/27 20:33:15 leavens Exp $
Invariant_Visible(Loc,T): trait
  includes TypedObj(Loc, T)
  assumes visible, i_pred(Loc,T)
  asserts
    \forall o: Loc[T], st: State
      (assigned(o,st) /\ visible(st)) => invariant_pred(o,st);

The notion of a visible state is not formalized here, but the signature of the trait function visible is given by the following. Note that visible(pre) and visible(post) should both be true for client functions, and for public member functions of a class.

% @(#)$Id: visible.lsl,v 1.1 1997/01/27 20:33:15 leavens Exp $
visible: trait
  includes State
  introduces
    visible: State -> Bool

The other trait used in this semantics, written as ITranslation in the example above, is generated from the particular predicate in the invariant-clause. Each such trait translates the invariant's predicate into a trait that defines the trait function invariant_pred. This trait function must have the signature described by the two instantiations of the following trait, which is assumed by the instantiations of Invariant_Visible.

% @(#)$Id: i_pred.lsl,v 1.1 1997/01/27 20:33:15 leavens Exp $
i_pred(Loc,T): trait
  assumes TypedObj(Loc,T)
  introduces
    invariant_pred: Loc[T], State -> Bool

The translation would use the eval trait function from the trait TypedObj, so that, for example, occurrences of self\any would become eval(self, any). Hence the signature given above.

As an example of this translation, consider again the rewritten invariant from Person given above. The generated trait for this invariant might be expressed as follows.

% @(#)$Id: PTranslation.lsl,v 1.1 1997/01/27 20:43:27 leavens Exp $
PTranslation: trait
  includes PersonInvariant(Obj), PersonInvariant(ConstObj)

The above trait just includes the following trait twice, once for regular and constant objects. In the following trait, we make use of the fact that self and any are not reserved words in LSL to make the translation be as close as possible to the original predicate.

% @(#)$Id: PersonInvariant.lsl,v 1.2 1997/07/30 22:07:40 leavens Exp $
PersonInvariant(Loc): trait
  includes i_pred(Loc,Person), Person_Trait
  asserts
    \forall self: Loc[Person], any: State
      invariant_pred(self, any)
        == len(eval(eval(self,any).name, any)) > 0
           /\ eval(eval(self,any).age, any) >= 0;

In the general case, an invariant may involve static variables and global variables. The idea of the formalization for these cases is the same except that no rewriting using self is involved. We omit the formal details for the sake of brevity.

An invariant-clause may appear anywhere a member-declaration may appear in a class specification. See section 7 Class Specifications for the details of the syntax. We suggest that normally you write it near the top of the class specification. You can write multiple invariants in a class specification; this is just a shorthand for writing the conjunction of the given invariants. See section 10.3 Specifying Protected and Private Interfaces for how one can use the flexibility of syntax.


Go to the first, previous, next, last section, table of contents.