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


6.3.2.1 Trashed

An lcpp-primary such as trashed(t1,t2) can be used in a specifying a function that must deallocate or "finalize" an object. It can also be used in specifying C++ destructors for type of objects whose abstract values contains objects that are visible to clients. (See section 7.2.2 Destructors for discussion and examples. Note, however, that in Larch/C++, it is a mistake to write trashed(self) in a postcondition.)

An lcpp-primary of the form trashed(term-list) can only be used in the postcondition. Furthermore, all objects described by the term-list must be described by the store-ref-list in the function's trashes-clause (see section 6.3.2 The Trashes Clause).

The lcpp-primary trashed(t1,t2) states that the objects t1 and t2 are to be either uninitialized or deallocated. Formally it is translated into the following term.

  (isTrashed(t1, pre, post) /\ isTrashed(t2, pre, post))

(5) See section 6.3.2.2 Formal Details of the Trashes Clause for the trait function isTrashed.

The sort of trashed(term-list) is Bool.

A simple example is the following specification. It must be implemented by a function that makes ir either unassigned or deallocated in the post-state.

// @(#)$Id: done_with.lh,v 1.5 1997/06/03 20:30:02 leavens Exp $

extern void done_with(int & ir) throw();
//@ behavior {
//@   trashes ir;
//@   ensures trashed(ir);
//@ }

Since trashed(x) does not necessarily mean that x is deallocated, one should use negation and the trait function allocated explicitly if one wishes to specify that an object must be deallocated, as opposed made unassigned. (See section 6.3.2 The Trashes Clause for an example.) Similarly, if one wishes to specify that objects must be made unassigned, then that can be stated using negation and the trait function unassigned. See section 6.2.2 Allocated and Assigned for details on these trait functions.

In the following example, when the reference count ref_count^ is 1, the object *cp is trashed, and otherwise it is not trashed.

// @(#)$Id: dec_ref.lh,v 1.7 1997/09/16 02:56:30 leavens Exp $
extern void dec_ref(char *cp, int & ref_count) throw();
//@ behavior {
//@   requires allocated(cp, pre) /\ assigned(ref_count, pre)
//@            /\ ref_count^ >= 1;
//@   modifies ref_count;
//@   trashes *cp;
//@   ensures ref_count' = ref_count^ - 1
//@           /\ (if ref_count' = 0 then trashed(*cp)
//@               else ~trashed(*cp));
//@ }

However, there are cases when one wants to leave it up to the implementation whether to deallocate or not. An example would be when one might want to let the implementation use a garbage collector. In such cases, one would just mention the objects in question in the trashes-clause but not specify that they must be trashed by using trashed in the postcondition.

An example is the function chaos, which terminates, but can have any effect [Nelson89] [Hesselink92]. (Such a function is not useful for much, but the specification demonstrates the expressiveness of Larch/C++.) The reason chaos can have any effect is that everything (every object) is threatened by the function, and everything can be both modified or trashed (but is not required to be modified or trashed).

// @(#)$Id: chaos.lh,v 1.4 1997/06/03 20:29:58 leavens Exp $

extern void chaos();
//@ behavior {
//@   extern everything;
//@   modifies everything;
//@   trashes everything;
//@   ensures true;
//@ }

The terms in the term-list passed to trashed should usually be of sort Set[TypeTaggedObject] or have the form Obj[T] or ConstObj[T]; as with fresh, as a syntactic sugar, terms of a sort for which the trait function contained_objects is defined may also be used as arguments to trashed. A set of objects is extracted from these terms in exactly the same way as for fresh (see section 6.3.1 Fresh), and for each such object o it is asserted that isTrashed(o,pre,post). See section 6.3.1 Fresh for the details of the syntactic sugars that apply.


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