8.3 Instantiation of Templates

The syntax for the instantiation of a template adds to the C++ syntax the ability to pass traits to an instantiation. The traits passed would be those expected by a template; that is those that are mentioned in an expects-clause. See section 5.2.3 Type Specifiers for the syntax of type-specifier. See section 5.4 Declarators for the syntax of abstract-declarator. See section 6.13 Specifying Higher-Order Functions for the syntax of using-trait-list.

template-instance ::= template-class-instance | template-non-class-instance
template-class-instance ::= template-class-name template-instance-actuals
template-non-class-instance ::= template-non-class-name template-instance-actuals
template-instance-actuals ::= < [ template-argument-list ] [ using-trait-list ] >
template-argument-list ::= template-argument [ , template-argument ] ...
template-argument ::= assignment-expression | type-id
        | [ :: ] [ nested-name-specifier ] template-class-name
        | [ :: ] [ nested-name-specifier ] template-non-class-name
type-id ::= type-specifier-seq [ abstract-declarator ]
explicit-instantiation ::= template declaration
explicit-specialization ::= template < > declaration

Each template-argument must match the type specified in the declaration of the template-class-name. To be legal, each template-argument that is a C++ type must be specified to satisfy any restrictions placed on it by the where-seq in the specification of the template-class-name. See section 8.2 Requirements on Template Parameters for details. Furthermore, the traits mentioned in the using-trait-list should satisfy the corresponding traits in the expects-clause in the template being instantiated. The expected traits are matched positionally.

For example, Stack<int /*@ using int @*/> and

 Stack<Stack<int /*@ using int @*/>
       /*@ using SimpleStackTrait(int, Stack<int>) @*/>

are both instances of the template class Stack (see section 8.1 Example Template without Requirements). However, the second instantiation is not legal (see section 8.2 Requirements on Template Parameters for the specification against which this statement is made), unless the operator == required by the template Set is provided for the type Set<int>.

Since the trait used for a class template depends on the actual parameters that instantiate the template, in order to write specifications as a client of a class template, one must give a uses-clause for each instance being used. In the following somewhat contrived example, the two uses-clauses are needed to give meaning to the appropriate overloadings of the trait functions used in the specification of pop_the_top_stack. These uses-clauses could also have been put within the fun-spec-body. Notice that when instantiating a template for LSL only, we do not give the using-trait-list.

// @(#)$Id: SimpleStackInstances.lh,v 1.6 1998/09/23 16:01:29 ruby Exp $
#include "SimpleStack.lh"

extern  Stack<Stack<int /*@ using int @*/>
              /*@ using SimpleStackTrait(int, Stack<int>) @*/>
          myStackofStacks;

//@ uses SimpleStackTrait(int for E, Stack<int> for C);
//@ uses SimpleStackTrait(Stack<int> for E, Stack< Stack<int> > for C);

extern void pop_the_top_stack() throw();
//@ behavior {
//@   requires assigned(myStackofStacks, pre) /\ ~isEmpty(myStackofStacks^)
//@            /\ ~isEmpty(top(myStackofStacks^));
//@   modifies myStackofStacks;
//@   ensures myStackofStacks' = push(pop(top(myStackofStacks^)),
//@                                   pop(myStackofStacks^));
//@ };

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