## 8.1 Example Template without Requirements

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 {}
\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