The syntax of the where-seq is as follows.
where-seq ::= where-clause [ where-clause ] ... where-clause ::=wheretype-arg-nameiscomplete-class-name;|wheretype-arg-nameiswhere-body;where-body ::= [class]{member-seq}type-arg-name ::= identifier | original-class-name | template-class-instance
Each where-clause in a where-seq constrains the
type-arg-name following the keyword where.
Each where-clause in a where-seq should constrain
a different type-arg-name,
and all the type-arg-names must be a type parameters.
These can be either identifiers following
the keyword class
in type-parameter or an instantiation of a class template
declared as a type-parameter.
Not every type parameter needs to be constrained in a where-clause;
leaving a type parameter unconstrained means that any actual
type (or template) argument is acceptable.
For example, the template Stack above
(see section 8.1 Example Template without Requirements)
can be instantiated with a type that is
not a class, such as int, as well as with class types.
There are three kinds of constraints that a where-clause can place
on a type argument. First two use the simplest syntactic form,
which involves the keyword is.
When the complete-class-name following is names a class,
as opposed to a signature,
then the actual argument must be a subtype of the given class name.
When the complete-class-name names a signature instead,
then the actual parameter must conform to the signature given.
To illustrate the use of subtyping,
consider the following example.
In it, Expr is a template class,
and the template function eval can work with any actual type
SI that is a subtype of the following.
SimpleStack<int using NoContainedObjects(int)>
That is one can instantiate eval
as follows
eval<Stack<int /*@ using NoContainedObjects(int) @*/>>
or as follows
eval<FastStack<int /*@ using NoContainedObjects(int) @*/>>
as long as FastStack is publicly derived from Stack.
This allows the function eval to treat SI as if it were exactly
SimpleStack<int using NoContainedObjects(int)>
in its body. Thus one has subtype polymorphism [Leavens-Weihl90] [Leavens91] [Leavens-Weihl95].
// @(#)$Id: eval.lh,v 1.9 1998/08/29 16:21:59 leavens Exp $
#include "SimpleStack.lh"
//@ uses SimpleStackTrait(int for E, Stack<int> for C);
template <class I>
class Expr;
//@ uses Eval_Trait(Expr<int>);
template <class SI>
//@ where SI is Stack<int using NoContainedObjects(int)>;
extern int eval(Expr<int> x, SI& stk) throw();
//@ behavior {
//@ requires isEmpty(stk^) /\ assigned(stk, pre);
//@ modifies stk;
//@ ensures result = final_value(x, stk^) /\ stk' = final_stack(x, stk^);
//@ }
The trait Eval_Trait used in this example is just a stub.
A more interesting specification would be needed in reality.
% @(#)$Id: Eval_Trait.lsl,v 1.1 1997/06/03 20:29:36 leavens Exp $
Eval_Trait(Expr): trait
assumes SimpleStackTrait(int, C), int
introduces
final_value: Expr, C -> int
final_stack: Expr, C -> C
If a signature is used instead of a class following is,
then the where-clause specifies that the actual
template argument must have a specification that conforms to
the given specification.
For the types, this means that the actual parameter has
all the operations of the given signature, and that
the types correspond [Baumgartner-Russo95].
The specification of each operation in the actual parameter must
also satisfy the given specification.
[[[Need to lay this out in detail]]]
For example, suppose we have the following signature defined.
This signature describes a type with an == operator defined on it.
All elements of a signature are implicitly public,
so there is no need to use the public: access specifier.
The expected trait must satisfy the specification Equality(Elem),
which the actual parameter trait must define the meaning of =.
The trait Equality is from Guttag and Horning's LSL handbook
(p. 193 of [Guttag-Horning93]).
// @(#)$Id: Equivalence.lh,v 1.3 1998/08/29 21:48:53 leavens Exp $
template <class Elem /*@ expects Equality(Elem) @*/>
signature Equivalence {
//@ bool operator ==(Elem x, Elem y);
//@ behavior {
//@ ensures returns /\ result = (x = y);
//@ }
};
Then we can use the above signature to describe the requirements on the
template parameter for a set template as follows.
The set template has an expected trait,
SimpleSetRequirement(Elem).
Note that there is a formal parameter name for this trait, ElemTrait,
since the actual parameter has to be passed to the instantiation of
the template signature Equivalence.
More discussion of this set template follows.
// @(#)$Id: SimpleSet2.lh,v 1.3 1998/09/24 16:36:45 leavens Exp $
#include "Equivalence.lh"
template <class Elem /*@ expects SimpleSetRequirement(Elem) ElemTrait @*/>
//@ where Elem is Equivalence<Elem using *ElemTrait>;
class Set {
public:
//@ uses SimpleSetTrait(Elem for E, Set<Elem> for C);
Set() throw();
//@ behavior {
//@ constructs self;
//@ ensures liberally self' = empty;
//@ }
void insert(Elem e) throw();
//@ behavior {
//@ modifies self;
//@ ensures liberally self' = self^ \U {e};
//@ }
bool is_in(Elem e) const throw();
//@ behavior {
//@ ensures result = (e \in self);
//@ }
};
In the Set template's where-clause,
the requirement is that Elem satisfy the following signature.
Equivalence<Elem using ElemTrait>
By the definition of Equivalence, this means that the type argument
Elem must have the C++ operator == defined
on it; furthermore == must have the expected behavior.
One can thus instantiate Set with types such as int
by writing Set<int /*@ using int ,
where the second
/>int is the name of the trait for the C++
type int
(see section 11.1.5 int Trait).
This makes the trait int the actual parameter
that must satisfy the required trait SimpleSetRequirement,
which is given below.
% @(#)$Id: SimpleSetRequirement.lsl,v 1.1 1998/08/29 21:48:37 leavens Exp $ SimpleSetRequirement(E): trait includes contained_objects(E), Equality(E)
However, an instantiation such as
Set<Set<int /*@ using int @*/> /*@using SimpleSetTrait(int, Set<int>)@*/>
is not legal
unless operator == is also specified
for the type Set<int /*@ using int @*/>.
The trait, SimpleSetTrait used in the interface specification
of the above example is as follows.
Note how it defines the trait function contained_objects
by using the trait container_objs defined above.
% @(#)$Id: SimpleSetTrait.lsl,v 1.2 1997/07/31 17:39:41 leavens Exp $
SimpleSetTrait(E, C): trait
includes ChoiceSet, container_objs(choose for head, rest for tail),
PureValue(C)
If a named signature is not needed, one can explicitly write out the description of the operations in the where-clause. Again, this kind of where-clause specifies that the actual template argument must have a specification that conforms to the given specification. This is just like the where-clause in Larch/CLU [Wing87]. For example, we could rewrite the simple set example above as follows.
// @(#)$Id: SimpleSet.lh,v 1.20 1998/08/29 21:48:54 leavens Exp $
template <class Elem /*@ expects SimpleSetRequirement(Elem) @*/>
//@ where Elem is {
//@ bool operator ==(Elem x, Elem y);
//@ behavior {
//@ ensures returns /\ result = (x = y);
//@ }
//@ };
class Set {
public:
//@ uses SimpleSetTrait(Elem for E, Set<Elem> for C);
Set() throw();
//@ behavior {
//@ constructs self;
//@ ensures liberally self' = empty;
//@ }
void insert(Elem e) throw();
//@ behavior {
//@ modifies self;
//@ ensures liberally self' = self^ \U {e};
//@ }
bool is_in(Elem e) const throw();
//@ behavior {
//@ ensures result = (e \in self);
//@ }
};
When the optional keyword class is used in this explicit
form of a where-body it specifies that the actual type parameter must
be a class type, not just any C++ type.
The use of the class keyword also enables all the syntax and
semantics of class specifications, allowing the use of self,
and the specification of constructors, destructors etc.
Normally one would, however, only specify public member functions,
and so one should use the keyword public: at the beginning.
As shown above, in general, the actual parameter must provide a trait
that matches the expected trait theory used in the specification
[Goguen84] [Ernst-etal91] [Edwards-etal94].
In Larch/C++, this theory is provided by the use of
the keyword using to pass traits that were
"expected".
See section 6.13 Specifying Higher-Order Functions for the syntax of
the expects-clause.
As a more complete example, we specify a priority queue.
Recall that a priority queue is a container with elements drawn from
a totally-ordered type.
We will provide an operation Largest to extract the largest
element, and an operation Insert to insert an element
into the priority queue.
A trait describing the theory of the elements is expected.
This trait, which is given below,
says that the actual trait parameter must
define the contained_objects trait function
and a total order on the elements.
For the trait giving the ordering on the elements,
we use the trait TotalOrder from section A.12 of [Guttag-Horning93].
% @(#)$Id: PriorityQueueRequirement.lsl,v 1.1 1998/08/29 21:48:36 leavens Exp $ PriorityQueueRequirement(E): trait includes contained_objects(E), TotalOrder(E for T)
For the abstract model of priority queues, we use the trait
PriorityQueueTrait, given below.
This uses the trait PriorityQueuefrom page 175 of [Guttag-Horning93].
% @(#)$Id: PriorityQueueTrait.lsl,v 1.2 1997/07/31 17:39:41 leavens Exp $
PriorityQueueTrait: trait
assumes TotalOrder(Elem for T)
includes PriorityQueue(Elem for E, PQ[Elem] for C),
container_objs(Elem for E, PQ[Elem] for C),
PureValue(PQ[Elem])
The specification of the template class PriorityQueue
uses an expects-clause to say that
a trait that satisfies PriorityQueueRequirement(Elem)
must be passed, as described above.
The operator <= specified in the where-clause
must be defined for the type Elem;
as it would be needed in the template class's implementation.
// @(#)$Id: PriorityQueue.lh,v 1.13 1998/09/23 16:02:04 ruby Exp $
template <class Elem /*@ expects PriorityQueueRequirement(Elem) @*/>
//@ where Elem is {
//@ bool operator <= (Elem x, Elem y);
//@ behavior {
//@ ensures returns /\ result = (x <= y);
//@ }
//@ };
class PriorityQueue {
public:
//@ uses PriorityQueueTrait(PriorityQueue<Elem> for PQ[Elem]);
PriorityQueue() throw();
//@ behavior {
//@ modifies self;
//@ ensures liberally self' = empty;
//@ }
PriorityQueue(const PriorityQueue<Elem>& oth) throw();
//@ behavior {
//@ modifies self;
//@ ensures liberally self' = oth\any;
//@ }
virtual ~PriorityQueue() throw();
//@ behavior {
//@ trashes self;
//@ ensures allocated(self, post);
//@ ensures redundantly assigned(self, post) => unchanged(self);
//@ example unchanged(self);
//@ example ~assigned(self,post);
//@ }
virtual void Insert(Elem e) throw();
//@ behavior {
//@ modifies self;
//@ ensures liberally self' = add(e, self^);
//@ }
virtual Elem Largest() const throw();
//@ behavior {
//@ requires len(self^) >= 1;
//@ ensures result = head(self^);
//@ }
virtual Elem RemoveLargest() throw();
//@ behavior {
//@ requires len(self^) >= 1;
//@ modifies self;
//@ ensures result = head(self^) /\ self' = tail(self^);
//@ }
virtual bool IsEmpty() const throw();
//@ behavior {
//@ ensures result = isEmpty(self\any);
//@ }
virtual long int Length() const throw();
//@ behavior {
//@ ensures liberally result = len(self\any);
//@ }
virtual long int Count(Elem e) const throw();
//@ behavior {
//@ ensures liberally result = count(self\any);
//@ }
};
The destructor in the above specification is somewhat interesting.
It is specified explicitly, because there are virtual functions
in the specification (see section 7.2.2 Destructors).
This particular specification allows an implementation
to trash the abstract value of self.
However, as a destructor cannot deallocate self
(that is the job of C++),
trashing in this instance simply permits the destructor to
make the abstract value become unassigned
(as the second example in the specification demonstrates).
See section 6.3.2 The Trashes Clause for details of the semantics of
the trashes-clause.
One final thing about the above specification. If the specification were written using subtype polymorphism, then the expects-clause would have been omitted, and the match of the actual-parameter theory to the formal parameter theory would have occurred during the proof of behavioral subtyping.
Go to the first, previous, next, last section, table of contents.