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.