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.