When an object is trashed, it can no longer be used. In the Larch/C++ model of C++, a function call can make this can happen in the following ways.
Functions that trash objects must include a trashes-clause-seq. If a trashes clause is not included, then the function may not trash any objects. If such a clause is included, then only the objects described may be trashed. An object is described by the trashes-clause if it is listed explicitly, or if it depends on a described object. This means that objects that are not described in the trashes-clause-seq cannot be made unassigned or deallocated. The objects described in the trashes-clause-seq do not have to be trashed, the point is that they are allowed to be trashed.
Because objects that are not described by the trashes-clause-seq are not allowed to be trashed, the postcondition of a function specification does not have to mention that all other objects stay allocated or assigned. Hence, the trashes-clause-seq, along with the modifies-clause-seq, gives a complete frame axiom [Borgida-etal95] for the function specification.
The idea of the trashes-clause-seq and its utility in making Larch-style specifications referentially transparent and less verbose is taken from Chalin [Chalin95].
The trashes-clause-seq has a syntax that is very similar to the syntax of the modifies-clause-seq.
trashes-clause-seq ::= trashes-clause [ trashes-clause ] ... trashes-clause ::=trashes[redundantly] store-ref-list;
See section 6.9.4 Redundancy in Frames for
the meaning of redundantly used in a trashes-clause.
When several non-redundant trashes-clauses are listed in
a trashes-clause-seq, this is the same as listing each of their
store-ref-lists in a single trashes-clause.
If more than one non-redundant trashes-clause is given,
then none of the store-ref-lists may be of the form
nothing or everything.
Because it is possible to translate multiple non-redundant
trashes-clauses into a single trashes-clause,
we will assume from now on that there is only one
non-redundant trashes-clause.
For example, the following specifies a function that deallocate an integer
object.
The requires-clause states that the pointer passed
must be a non-null pointer, and that it points to allocated storage.
(Equivalently, this could have been stated as allocated(p, pre),
see section 11.8 Pointer Types for the details of these trait functions.)
The trashes-clause says that the function is allowed to,
but does not have to, deallocate or make unassigned the object
*p.
The postcondition states that *p must be deallocated.
The redundant postcondition
follows from the meaning of ~allocated(p, post)
in the pointer traits.
(See section 6.9.3 Redundant Ensures Clauses or Claims for the
meaning of a redundant ensures-clause.)
// @(#)$Id: dealloc_int_obj.lh,v 1.7 1998/08/27 22:42:12 leavens Exp $
extern void dealloc_int_obj(int *p) throw();
//@ behavior {
//@ requires isValid(p) /\ allocated(*p, pre);
//@ trashes *p;
//@ ensures ~allocated(*p, post);
//@ ensures redundantly ~allocated(p, post);
//@ }
Other topics related to the trashes-clause are discussed below.
Go to the first, previous, next, last section, table of contents.