In a `trashes-clause` the same
sort restrictions and syntactic sugars apply as for the
`modifies-clause`.
Suffice it to say that each `store-ref`
should be a `term` whose sort is
`Set[TypeTaggedObject]`

or of the form `Obj[T]`

(or, as a syntactic sugar, a `term`

with a sort for which
the trait function `contained_objects`

is defined).
(See section 6.2.3.4 Formal Details of the Modifies Clause for details.)

The following summarizes the semantics of a
function specification with a `trashes-clause`.
First a set of type-tagged objects
is obtained from of the `trashes-clause`.
This set is closed to take dependencies into account.
Then this set is used to construct a predicate, TP,
which is conjoined to the written postcondition.

The set of type-tagged objects, UTTOs(`store-ref-list`),
is obtained from the `store-ref-list`
in a function's `trashes-clause` exactly
as with the `modifies-clause`.
Recall that this means
that UTTOs(`store-ref-list`) be the union of the sets TTO(SR)
of type tagged-objects that are the denotations
of each `store-ref` SR in the `store-ref-list`.
(See section 6.2.3.4 Formal Details of the Modifies Clause for details.)

Recall also that the set Closure(Env, UTTOs(`store-ref-list`)) is the
closure of this set so that all objects in the environment Env
on which the objects
in UTTOs(`store-ref-list`) depend (recursively) are added
(see section 7.6 The Depends Clause and Chapter 11 of [Leino95]).

Let TrashedObjects(`pre`

, `post`

) be the set
such that for each typed object sort, `Loc[T]`

,
and for each typed object `loc`

of sort `Loc[T]`

,
`widen(loc)`

is in TrashedObjects(`pre`

, `post`

)
if and only if `isTrashed(loc, pre, post)`

holds
in the theory of `TypedObj(Loc, T)`

.
This is summarized somewhat informally by the following.

TrashedObjects(`pre`

,`post`

) = {`widen(loc)`

|`isTrashed(loc, pre, post)`

,`loc`

is a typed object }

Recall that `isTrashed(loc, pre, post)`

is only true
if the type of `loc`

is a type recorded in the state `pre`

.
This prevents arbitrary type perspectives from affecting whether
an object is trashed.
Note that the notion of being trashed is typed,
because it depends on the notion of when an object is unassigned.
(However, this is just the way the notions fall out in the Larch/C++
traits; there is nothing essential about having this notion be typed.)

The predicate TP is then the following.
(Except for `\subseteq`

from the trait `Set`

, which
is defined in the LSL Handbook of [Guttag-Horning93],
the other trait functions are described following the predicate.)

TrashedObjects(pre, post) \subseteq ignoringTypeTags(Closure(Env, UTTOs(store-ref-list)))

In the above predicate, the type-tags in the set
Closure(Env, UTTOs(`store-ref-list`)) are not used.
However, the reason for having these type-tags is not
for the trashes clause, but for the semantics
of `reach`

(see section 6.2.3.5 Reach) and `unchanged`

(see section 6.2.3.6 Unchanged).
One does not want to compare type-tagged objects for the trashes clause,
as that would prohibit cross-type aliasing and many uses of subtyping.

The meaning of the trait function `isTrashed`

for each sort of the form `Loc[T]`

is given by the trait `TrashesSemantics(Loc, T)`

below.
This trait would be instantiated for each such sort,
so that it applies to the sort of `loc`

in the formula above.

% @(#)$Id: TrashesSemantics.lsl,v 1.2 1995/11/13 15:34:50 leavens Exp $ TrashesSemantics: trait assumes State, AllocatedAssigned(Loc, T) introduces isTrashed: Loc[T], State, State -> Bool asserts \forall loc: Loc[T], pre,post: State isTrashed(loc, pre, post) == (assigned(loc, pre) /\ ~assigned(loc, post)) \/ (allocated(loc, pre) /\ ~allocated(loc, post)); implies \forall loc: Loc[T], pre,post: State isTrashed(loc, pre, post) => (allocated(loc, pre) /\ (~allocated(loc, post) \/ ~assigned(loc, post))); isTrashed(loc, pre, post) => ~assigned(loc, post); ~isTrashed(loc, pre, post) == (~assigned(loc, pre) \/ assigned(loc, post)) /\ (~allocated(loc, pre) \/ allocated(loc, post)); (~isTrashed(loc, pre, post) /\ assigned(loc, pre)) => assigned(loc, post); (~isTrashed(loc, pre, post) /\ allocated(loc, pre)) => allocated(loc, post); converts isTrashed exempting \forall loc: Loc[T], st: State isTrashed(loc,bottom,st), isTrashed(loc,st,bottom)

See section 2.8.2 Formal Model of States for the assumed trait `State`

.
See section 6.2.2 Allocated and Assigned for the assumed trait
`AllocatedAssigned`

.
See section 2.8.1 Formal Model of Objects for the
trait `TypedObj`

which includes `ModifiesSemantics`

.

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