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.