6.3.2.2 Formal Details of the Trashes Clause

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.