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


7.5 Contained Objects

Larch/C++ relies on the specifier of a class whose abstract values are explicitly given by a LSL trait to tell it what objects may be contained in the abstract values of a class. This is needed to give meaning to the lcpp-primary reach(x) (see section 6.2.3.5 Reach), and in various other syntactic sugars. Therefore, when explicitly specifying the abstract values of a class with an LSL, as opposed to using specification variables, one needs to give some thought to whether the abstract values themselves contain objects. Once this is decided, the trait function contained_objects should be defined to tell Larch/C++ about any contained objects in the abstract value, along with their types.

The signature required for the trait function is given by the following trait. (See section 6.2.3 The Modifies Clause for the trait TypeTaggedObject.)

% @(#)$Id: contained_objects.lsl,v 1.9 1995/11/10 06:47:25 leavens Exp $
% Assumption about the sort of contained_objects, and useful includes
contained_objects(T): trait
  includes State, TypeTag(T)
  introduces
    contained_objects: T, State -> Set[TypeTaggedObject]

Often the abstract values of a class do not contain any objects, only pure values. In this case, defining the contained_objects trait function is easy. One simply includes the LSL trait NoContainedObjects, with an appropriate renaming or sort parameter. For example, in specifying the class Money (see section 7.1.2 A Design with a Nontrivial Trait (Money)), we used the trait NoContainedObjects(Money). The trait NoContainedObjects is defined as follows.

% @(#) $Id: NoContainedObjects.lsl,v 1.18 1997/07/31 01:31:45 leavens Exp $

NoContainedObjects(V) : trait
  includes PureValue(V),         % defines eval, allocated, assigned
           contained_objects(V)  % gives sort assumption
  asserts
    \forall v: V, st: State
    contained_objects(v, st) == {};

Besides defining the trait function contained_objects, this trait also defines three other trait functions, as described by the following trait. These help with various defaults in Larch/C++, specifically they make sense out of the default copy constructor and the default assignment operator (see section 7.2.3 Implicitly Generated Member Specifications), and they make sense out of the implicit preconditions for member functions of a class (see section 6.2.2 Allocated and Assigned).

% @(#) $Id: PureValue.lsl,v 1.1 1997/07/31 01:31:46 leavens Exp $

PureValue(V) : trait
  assumes State
  introduces
    eval: V, State -> V
    allocated, assigned: V, State -> Bool
  asserts
    \forall v: V, st: State
    eval(v, st) == v;
    allocated(v, st);
    assigned(v, st);

To define one's own version of the trait function contained_objects, one uses the trait function asTypeTaggedObject from the following trait.

% @(#)$Id: TypeTag.lsl,v 1.4 1995/11/10 06:46:58 leavens Exp $
TypeTag(T): trait
  assumes State, WidenNarrow(T, Object)
  includes TypeTaggedObject, IgnoringTypeTags,
           SortNames(T, TYPE, type_of for sort_of)
  introduces
    asTypeTaggedObject: T -> TypeTaggedObject
  asserts
    \forall o: T
      asTypeTaggedObject(o) == [widen(o), type_of(o)];
  implies
    \forall o: T
      asTypeTaggedObject(o).obj == widen(o);

See section 6.2.3.4 Formal Details of the Modifies Clause for IgnoringTypeTags. The trait SortNames is given below. It specifies a metalogical operation, sort_of, that is supposed to reify sorts in LSL. This operation is not completely formalized here.

% @(#)$Id: SortNames.lsl,v 1.2 1997/01/27 21:04:28 leavens Exp $
% A reification of sort names in LSL
SortNames(S, SORTNAME): trait
  introduces 
    sort_of: S -> SORTNAME
  asserts
    \forall s, s1: S
      sort_of(s) == sort_of(s1);

For an example of a class with abstract values that contain objects, we will specify a class PersonSet. This class will have abstract values that are Person objects (see section 7.1.1 A First Class Design (Person) for the specification of Person). A PersonSet, as a set of objects, may contain two distinct Person objects with the same abstract value. This reflects the reality that, just because two people have the same name and age, does not mean that they are identical.(7) Therefore, for the abstract values of PersonSet, we use the LSL Handbook trait Set (page 167 of [Guttag-Horning93]), but for the elements we use Obj[Person], not Person. Hence we write the following trait. This trait adds the trait functions contained_objects, eval, allocated, and assigned to the trait functions defined in the included traits. (See section 2.8.1 Formal Model of Objects for the trait MutableObj. See section 7.1.1 A First Class Design (Person) for the trait Person_Trait.) Specifying the trait function eval allows one to write self" to mean the set of values of the objects in the post-state value of self. We make the trait functions allocated and assigned always return true for PersonSet values, so that the implicit preconditions of member functions (see section 6.2.2 Allocated and Assigned) do not require these objects to be assigned.

% @(#)$Id: PersonSetTrait.lsl,v 1.12 1997/07/31 02:43:26 leavens Exp $
PersonSetTrait: trait
  includes Person_Trait, MutableObj(Person),
           Set(Person, Set[Person]),
           Set(Obj[Person], Set[Obj[Person]]),
           contained_objects(Set[Obj[Person]])
  introduces
    eval: Set[Obj[Person]], State -> Set[Person]
    allocated, assigned: Set[Obj[Person]], State -> Bool

  asserts
   \forall pv: Person, p: Obj[Person], s: Set[Obj[Person]], st: State
      asTypeTaggedObject(p) \in contained_objects(s, st) == p \in s;
      pv \in eval(s, st) == \E p (p \in s /\ eval(p, st) = pv);
      allocated(s, st);
      assigned(s, st);

Once this is decided, the interface specification of PersonSet can be written. An interface specification follows, which is discussed further below.

// @(#)$Id: PersonSet.lh,v 1.30 1997/07/31 02:43:26 leavens Exp $
#include "Person.lh"

//@ uses PersonSetTrait(PersonSet for Set[Obj[Person]]);

class PersonSet {
public:
  //@ invariant \A p: Obj[Person] ((p \in (self\any)) => assigned(p, any));

  PersonSet() throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = {};
  //@ }

  virtual ~PersonSet() throw();
  //@ behavior {
  //@   ensures true; // persons in self not deleted
  //@ }

  virtual void add(Person& e) throw();
  //@ behavior {
  //@   requires assigned(e, pre);
  //@   modifies self;
  //@   ensures self' = self^ \U {e};
  //@ }

  virtual void remove(Person& e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = delete(e, self^);
  //@ }

  virtual bool member(Person& e) const throw();
  //@ behavior {
  //@   ensures result = (e \in self^);
  //@ }

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

  virtual void bump_years() throw();
  //@ behavior {
  //@   requires \A p: Obj[Person] ((p \in (self\any)) => assigned(p, pre));
  //@   modifies contained_objects(self, any);
  //@   ensures \A p: Obj[Person]
  //@            ((p \in (self\any))
  //@             => (p'.age' = p^.age^ + 1 /\ p'.name' = p^.name^));
  //@   example \E p1: Obj[Person], p2: Obj[Person]
  //@             (assigned(p1, pre) /\ assigned(p2, pre)
  //@              /\ self^ = {p1} \U {p2} /\ p1^.age^ = 19 /\ p2^.age^ = 27
  //@              /\ self' = {p1} \U {p2} /\ p1'.age' = 20 /\ p2'.age' = 28
  //@              /\ p1'.name' = p1^.name^ /\ p1'.name' = p1^.name^);
  //@ }

  PersonSet& copy() const throw();
  //@ behavior {
  //@   requires \A p: Obj[Person] ((p \in (self\any)) => allocated(p, pre));
  //@   ensures fresh(result, contained_objects(result, post))
  //@           /\ assigned(result, post)
  //@           /\ result" = self\any\any;
  //@   example \E p1: Obj[Person], p2: Obj[Person],
  //@                   p1new: Obj[Person], p2new: Obj[Person]
  //@             (assigned(p1, pre) /\ assigned(p2, pre)
  //@              /\ self\any = {p1} \U {p2}
  //@              /\ p1\any.age = 19 /\ p1\any.name = A"fred"
  //@              /\ p1\any.age = 27 /\ p1\any.name = A"sue"
  //@              /\ fresh(result, p1new, p2new)
  //@              /\ result' = {p1new} \U {p2new}
  //@              /\ p1new'.age = 19 /\ p1new'.name = A"fred"
  //@              /\ p1new'.age = 27 /\ p1new'.name = A"sue");
  //@ }

  PersonSet& copy1() const throw();
  //@ behavior { // one-level copy
  //@   ensures fresh(result) /\ assigned(result, post)
  //@           /\ result' = self\any;
  //@   example \E p1: Obj[Person], p2: Obj[Person]
  //@             (self\any = {p1} \U {p2}
  //@              /\ fresh(result) /\ result' = {p1} \U {p2});
  //@ }
};

Notice that in the specification of PersonSet, reference parameters are used to pass Person objects, instead of Person values. For example, the sort of e in the member function add is Obj[Person] (see section 6.1.8.1 Sorts for Formal Parameters).

The specification of the member function bump_years deserves some comment. Notice that the abstract value of self is not changed by bump_years; what is changed are the abstract values of all the Person objects contained in self. To specify this, the function contained_objects is used in the modifies-clause (see section 6.2.3 The Modifies Clause). The postcondition is stated using a quantification over person objects (person values would not do).

The specifications of the member functions copy and copy1 make an interesting contrast. The function copy makes a copy both of self and the contained Person objects; this is why the notation self\any\any is used. The function copy1 returns a newly allocated PersonSet object, but this set shares the contained objects that are its elements with self.


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