7.4 History Constraints

The constraint-clause specifies a property of on the history of values which an assigned object may take [Liskov-Wing93b] [Liskov-Wing94]. For example, in the specification of Person (see section 7.1.1 A First Class Design (Person)), the constraint says that a person's age can only increase. Such specifications are particularly useful for specifying abstract classes, where there are no constructors [Liskov-Wing93b] [Liskov-Wing94]. They may also be used to state properties such as that the assigned objects of a class are immutable, or that certain parts of the abstract value do not change or change monotonically. For example, in the specification of Money (see section 7.1.2 A Design with a Nontrivial Trait (Money)), the constraint says that an assigned Money object's abstract value never changes, hence money objects are immutable.

The syntax is as follows. The optional constrained-set allows a constraint to be stated that only applies to the functions listed.

constraint-clause ::= constraint [ redundantly ] predicate [ constrained-set ] ;
constrained-set ::= for fun-interface-list
fun-interface-list ::= fun-interface [ , fun-interface ] ...
        | nothing | everything

Ignoring the constrained-set for the moment, a history constraint specifies a relationship between each pair of visible states ordered in time. (See section 6.2.1 State Functions for a definition of visible state.) This relationship must be both reflexive and transitive.

For example, the first state might be the state just before calling some public member function, and the latter state might be the state just after the call returns. Hence the two states will be referred to as the "pre-state" and the "post-state". However, in general the two states do not have to be the pre- and post-states of a call, the "pre-state" just has to occur before the "post-state" in the execution of the program [Liskov-Wing93b] [Liskov-Wing94].

In a history constraint, one can use the state-functions ^ and \pre to refer to an assigned object's value in the "pre-state", and ' and \post to refer to such a value in the "post-state". For example, recall the history constraint from the specification of the class Money (see section 7.1.2 A Design with a Nontrivial Trait (Money)). This history constraint, given below, says that the abstract values of assigned Money objects do not change over time.

  constraint self^ = self';

Therefore this is a way of saying that Money objects are immutable.

As with invariants, it may be helpful to think of a history constraint as being manifested for assigned objects in redundant ensures-clauses of public member functions. That is, the history constraint is a property that is added to the theory of pairs of visible states for objects of the type. For example, if constraint_predicate(self, pre, post) is the given predicate, then for each pair of visible states such that pre precedes post in an execution, the following must hold.

(assigned(self, pre) => constraint_predicate(self, pre, post))

Although the constraint can be made manifest through redundant claims in member function specifications, the constraint is not necessarily redundant with the specifications given in the class. Instead, the constraint is an additional obligation that must be met by an implementation of the class.

Redundancy can also be used to help debug history constraints. A history constraint 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 history constraints.

If a function is specified in a way that would force a correct implementation to violate the history constraint, then the function will not be correctly implementable. Similarly, the class as a whole must preserve the constraints to be correctly implementable.

As with invariants, the formal semantics of a history constraint can be given by translating it into the use of two traits. The uses-clause, exemplified by the one given below, would appear outside any class declaration in which the constraint-clause appears. The first trait used is always HistoryConstraint(T), where the sort of self is Obj[T]. The second trait, written as HCTranslation below, would be different each time; it would be generated for each constraint clause as described below.

//@ uses HistoryConstraint(T), HCTranslation;

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

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

The trait Constraint_Visible that is included by the above is the following. This trait states that if an object is assigned in two visible states, then the history constraint predicate, constraint_pred is satisfied by that object in the two states. 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: Constraint_Visible.lsl,v 1.1 1997/01/27 20:33:15 leavens Exp $
Constraint_Visible(Loc,T): trait
  includes TypedObj(Loc, T)
  assumes visible, follows, c_pred(Loc,T)
  asserts
    \forall o: Loc[T], pre, post: State
      (assigned(o,pre) /\ assigned(o,post)
                       /\ visible(pre) /\ visible(post)
                       /\ follows(pre, post))
         => constraint_pred(o,pre,post);

See section 7.3 Class Invariants for the trait visible.

The notion of one state following another in a computation is not formalized here, but the signature of the trait function follows is given by the following trait. Note that follows(pre, post) should be true for any function.

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

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

% @(#)$Id: c_pred.lsl,v 1.2 1997/01/27 20:35:17 leavens Exp $
c_pred(Loc,T): trait
  assumes TypedObj(Loc,T)
  introduces
    constraint_pred: Loc[T], State, State -> Bool

The translation would use the eval trait function from the trait TypedObj, so that occurrences of self^ would become eval(self, pre), and occurrences of self' would become eval(self, post).

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

% @(#)$Id: MTranslation.lsl,v 1.1 1997/01/27 20:43:27 leavens Exp $
MTranslation: trait
  includes MoneyConstraint(Obj), MoneyConstraint(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, pre, and post are not reserved words in LSL, so that the translation is close as possible to the original predicate.

% @(#)$Id: MoneyConstraint.lsl,v 1.1 1997/01/27 20:43:27 leavens Exp $
MoneyConstraint(Loc): trait
  includes c_pred(Loc,Money), MoneyTrait
  asserts
    \forall self: Loc[Money], pre, post: State
      constraint_pred(self, pre, post)
        == eval(self,pre) = eval(self,post);

In a constraint-clause, the optional constrained-set lists a number of member functions or friend functions. The same function must not appear twice in the list, and only member and friend functions may be listed. A constrained-list of the form for everything is similar to listing all the member and friend functions (except for the basic constructors), but applies to all member and friend functions, even when new ones are added. This has an effect on public subclasses as well, as the constraint applies to all of their member functions by specification inheritance (see section 7.9 Inheritance of Specifications and Subtyping). An omitted constrained-list is shorthand for writing a constrained-set of the form for everything.

With a constrained-set that explicitly lists various member and friend functions, the history constraint has a more limited meaning. It says that the constraint must hold for every assigned object which is manipulated using only the listed functions. (In terms of the semantics given above, this means that follows(pre, post) should not hold if the transformation from pre to post involves a call of a member or friend function that is not listed.)

History constraints with constrained-sets can also be used to say that certain attributes of an object are not changed by certain member or friend functions.

As an example, consider the following specification of the class Person2. In this class the first history constraint applies to all member functions (except the constructors), but the rest have a constrained-set.

The second history constraint says that the member functions name and years_old do not change the abstract value of an object of class Person. Without the listed constrained-set, the constraint would contradict other parts of the specification. (Whole interfaces of functions must be used because C++ allows overloading.)

The third history constraint says that change_name does not change the age of a Person2 object. Note that it conjoining the predicate age' = age^ to the postcondition of change_name would be equivalent. (This is an example of the idea for understanding history constraints described above.) The fourth history constraint says that make_year_older does not change the name of a Person2 object.

// @(#)$Id: Person2.lh,v 1.14 1998/08/27 22:42:09 leavens Exp $

#include "AbstractString.lh"

//@ uses cpp_string;

class Person2 {
public:
  //@ spec int age;             // age interpreted as number of years old
  //@ spec String<char> name;

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

  //@ constraint age^ <= age';  // age can only increase
  //@ constraint name^ = name' /\ age^ = age'
  //@    for virtual char * name() const,
  //@        virtual int years_old() const;
  //@ constraint age' = age^
  //@    for virtual void change_name(const char *);
  //@ constraint name' = name^
  //@    for virtual void make_year_older();

  Person2(const char *moniker, int years) throw();
  //@ behavior {
  //@   requires nullTerminated(moniker,pre) /\ lengthToNull(moniker,pre) > 0
  //@            /\ years >= 0;
  //@   modifies name, age;
  //@   ensures name' = uptoNull(moniker,pre) /\ age' = years;
  //@ }

  virtual ~Person2() throw();
  //@ behavior {
  //@   ensures true;
  //@ }

  virtual void Change_Name(const char *moniker) throw();
  //@ behavior {
  //@   requires nullTerminated(moniker,pre) /\ lengthToNull(moniker,pre) > 0;
  //@   modifies name;
  //@   ensures name' = uptoNull(moniker,pre);
  //@   ensures redundantly len(name') > 0;
  //@ }

  virtual char * Name() const throw();
  //@ behavior {
  //@   ensures nullTerminated(result,post)
  //@           /\ fresh(objectsToNull(result,post))
  //@           /\ uptoNull(result,post) = name\any;
  //@ }

  virtual void Make_Year_Older() throw();
  //@ behavior {
  //@   requires age^ < INT_MAX;
  //@   modifies age;
  //@   ensures age' = age^ + 1;
  //@   example age^ = 29 /\ age' = 30;
  //@ }

  virtual int Years_Old() const throw();
  //@ behavior {
  //@   ensures result = age\any;
  //@ }
};

Note that second, third, and fourth history constraints of Person2 are redundant, in the sense that they already follow from the modifies-clauses of the relevant functions.

The first history constraint in Person2 is redundant in a sense, because one can recover it from an analysis of the specification; however it is a property of the class as a whole.

History constraints are also not redundant in the specification of abstract classes (see section 7.10 Abstract Classes).

One way to check that a class satisfies a history constraint is to check that the pre- and post-states of each member and friend function listed in the constrained-set satisfy it, and to ensure that the class's abstraction barrier is never violated. (This is called the history rule in [Liskov-Wing94].) If the constrained-set is for everything or omitted, then this restriction must, of course, be satisfied by all the member and friend functions. (Note, however, that the basic constructors, for which self is not assigned in the pre-state, trivially satisfy the constraint with respect to self.)

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