The template class Stack specified below
is an example of the specification of a template class.
This example is simple in the sense that it has minimal expectations
of its type parameter.
It does, however, illustrate some of the subtle features of working
with contained objects in a template.
The expects-clause below says that the trait
contained_objects(T) (see section 7.5 Contained Objects)
must be passed as a trait actual parameter when this template
is instantiated.
A discussion on how this expected trait
is used to define contained_objects
for instances of the Stack template is found after the example.
// @(#)$Id: SimpleStack.lh,v 1.18 1998/09/23 16:01:14 ruby Exp $
template <class T /*@ expects contained_objects(T) @*/ >
class Stack {
public:
//@ uses SimpleStackTrait(T for E, Stack<T> for C);
Stack() throw();
//@ behavior {
//@ constructs self;
//@ ensures liberally self' = empty;
//@ }
void push(T e) throw();
//@ behavior {
//@ modifies self;
//@ ensures liberally self' = push(e, self^);
//@ }
T pop() throw();
//@ behavior {
//@ modifies self;
//@ ensures self' = pop(self^);
//@ }
T top() const throw();
//@ behavior {
//@ requires ~isEmpty(self^);
//@ ensures result = top(self^);
//@ }
};
An instantiation of SimpleStack,
such as the following
SimpleStack<int& /*@ using MutableObj(int) @*/>
must pass a trait that satisfies the specification
of the expected trait, when the actual parameters are substituted for
the formals.
In this case, the LSL sort for int& is Obj[int],
and thus the trait expected is contained_objects(Obj[int]).
The actual trait passed, MutableObj(int)
satisfies the theory of this expected trait.
See section 8.3 Instantiation of Templates for more about instantiations.
Note that the uses-clause for this example is, contrary to our
usual practice to this point, found inside the class definition.
This is because the trait used depends on the particular type parameter.
Trying to put the uses clause outside the template definition
would result in an error, because then the type parameter T
would not be visible as a type.
However, because the trait used depends on the type parameter,
clients that instantiate Stack will themselves have to
use an appropriate trait.
(See section 8.3 Instantiation of Templates for an example.)
The trait for SimpleStack is given below.
It simply uses the trait Stack from Guttag and Horning's
LSL Handbook (page 170 of [Guttag-Horning93]),
and specifies the trait function contained_objects.
It includes the trait PureValue(C) to specify that
eval on stack values should be the identity function
(see section 6.2.1 State Functions),
and that the potential subobjects within a stack should not
affect the implicit preconditions for member functions
(see section 6.2.2 Allocated and Assigned).
See section 7.5 Contained Objects for the trait PureValue.
% @(#)$Id: SimpleStackTrait.lsl,v 1.2 1997/07/31 04:02:26 leavens Exp $
SimpleStackTrait(E, C): trait
includes Stack, container_objs(top for head, pop for tail),
PureValue(C)
The trait container_objs
is often useful in specifying
templates that are containers.
(In this context, a container is an object whose abstract values
satisfy the LSL Handbook trait Container,
see page 177 of [Guttag-Horning93].)
It defines the contained objects of a stack to be the contained objects
of the elements of the stack.
For example, if the actual template parameter used for T
is an object type, such as int&,
then all of those elements of the stack will be contained objects.
Similarly, if the actual template parameter used for T
is an pointer type, such as int *,
then the objects pointed at by the elements of the stack
will be the contained objects.
% @(#)$Id: container_objs.lsl,v 1.8 1995/08/24 17:31:16 leavens Exp $
% This trait is useful for defining contained_objects for generic containers,
% such as Set<T>, List<T>, etc.
container_objs(E,C): trait
includes contained_objects(C) % introduces the signature
assumes Container(E,C), contained_objects(E)
asserts
\forall e: E, c: C, st: State, o: Object
contained_objects(c, st)
== if isEmpty(c) then {}
else contained_objects(head(c), st)
\U contained_objects(tail(c), st)
implies
with_member_objs(E,C)
converts contained_objects: C, State -> Set[TypeTaggedObject]
If one has a sort of abstract values with a membership test,
but nothing like the trait functions head and tail,
then one can use the following weaker trait instead of container_objs.
% @(#)$Id: with_member_objs.lsl,v 1.4 1995/08/23 22:58:34 leavens Exp $
% This trait is useful for defining contained_objects for generic containers,
% such as Set<T>, List<T>, etc, for which the trait function \in is defined.
% See container_objs for a stronger trait that assumes more.
with_member_objs(E,C): trait
includes contained_objects(C)
assumes HasMembership(E,C), contained_objects(E)
asserts
\forall e: E, c: C, st: State
(e \in c)
=> (contained_objects(e,st) \subseteq contained_objects(c, st))
The trait HasMemberhip assumed by the above trait is
given below.
% @(#)$Id: HasMembership.lsl,v 1.1 1994/12/08 21:39:46 leavens Exp $
HasMembership(E,C): trait
introduces
__ \in __ : E, C -> Bool
Go to the first, previous, next, last section, table of contents.