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

6.2.3.4 Formal Details of the Modifies Clause

A store-ref can be any 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 2.8.1 Formal Model of Objects for sorts of the form Obj[T] and ConstObj[T]. See section 6.2.3.5 Reach for the sort requirements of arguments to reach.

The sort TypeTaggedObject is defined in the following trait. The sort TYPE in that trait represents the Larch/C++ sort of the object, which would have the form Obj[T] or ConstObj[T] for some C++ type T. (See section 2.8.1 Formal Model of Objects for the sorts Obj[T] and ConstObj[T]. See section 2.8.2 Formal Model of States for the sort Object.) 

% @(#)$Id: TypeTaggedObject.lsl,v 1.6 1995/11/09 23:02:43 leavens Exp $
TypeTaggedObject(TYPE): trait
  TypeTaggedObject tuple of obj: Object, type_tag: TYPE

The following summarizes the semantics of a function specification with a modifies-clause. First a set of type-tagged objects is obtained from the modifies-clause. Then the closure of this set is used to expand the set by including dependent objects [Leino95]. Then this set is used to construct a predicate, MP, 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 modifies-clause as follows. If the store-ref-list is nothing, then UTTOs(store-ref-list) = {}. If the store-ref-list is everything, then UTTOs(store-ref-list) is the set of all type-tagged objects that are allocated in the pre-state. Otherwise, let SR be a store-ref in the store-ref-list of the modifies-clause. Let TTO(SR) be a Set[TypeTaggedObject] defined as follows.

It is an error for a set TTO(SR) to be empty. Then, in the case where store-ref-list is not nothing or everything, UTTOs(store-ref-list) is the union of the sets TTO(SR) for each store-ref SR in the store-ref-list.

Let Closure(Env, UTTOs(store-ref-list)) be 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 ModifiedObjects(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 ModifiedObjects(pre, post) if and only if isModified(loc, pre, post) holds in the theory of TypedObj(Loc, T). This is summarized somewhat informally by the following. 

ModifiedObjects(pre, post)
   = { widen(loc) | isModified(loc, pre, post), loc is a typed object }

The predicate isModified(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 modified. Note that the notion of modification is essentially typed, because it depends on the notion of equality of abstract values, which is defined by the trait that specifies those abstract values. It would be wrong, and tantamount to comparing bits, to have defined this notion on untyped values.

The predicate MP 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.) 

ModifiedObjects(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 modifies 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 modifies clause, as that would prohibit cross-type aliasing and many uses of subtyping.

The meaning of the trait function modified for each sort of the form Loc[T] is given by the trait ModifiesSemantics(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: ModifiesSemantics.lsl,v 1.16 1995/11/13 15:38:59 leavens Exp $
% This is based on Chalin's help and his work [Chalin95].
ModifiesSemantics(Loc, T): trait
  assumes  State, AllocatedAssigned(Loc, T), TypedObjEval(Loc, T)

  introduces 
    isModified: Loc[T], State, State -> Bool

  asserts
    \forall loc: Loc[T], pre,post: State
      isModified(loc, pre, post)
        == (assigned(loc, pre) /\ assigned(loc, post)
               /\ eval(loc,pre) ~= eval(loc,post))
           \/ (allocated(loc, pre) /\ ~assigned(loc, pre)
               /\ assigned(loc,post));

  implies
    \forall loc: Loc[T], pre,post: State
      isModified(loc, pre, post)
         => (allocated(loc, pre) /\ assigned(loc, post));
    converts isModified
      exempting \forall loc: Loc[T], st: State
        isModified(loc,bottom,st), isModified(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.

The trait function ignoringTypeTags is defined by the following trait. 

% @(#)$Id: IgnoringTypeTags.lsl,v 1.1 1995/11/09 23:08:47 leavens Exp $
IgnoringTypeTags(TYPE): trait
  assumes TypeTaggedObject(TYPE)
  includes Set(Object, Set[Object], int for Int),
           Set(TypeTaggedObject, Set[TypeTaggedObject], int for Int)
  introduces 
    ignoringTypeTags: Set[TypeTaggedObject] -> Set[Object]
  asserts
    \forall stto: Set[TypeTaggedObject], tto: TypeTaggedObject
      ignoringTypeTags({}) == {};
      ignoringTypeTags(insert(tto, stto))
        == insert(tto.obj, ignoringTypeTags(stto));

Ignoring redundancy, and the trashes-clauses and calls-clauses, the meaning of a function specification with a modifies-clause is the following. A C++ function satisfies its specification if and only if for each type-correct function call, if the precondition predicate is satisfied in the pre-state, then the function call terminates, the function mutates at most the set of objects described in the modifies-clause, and the postcondition is satisfied by the pre-state and the post-state. (It should be understood that the desugared forms are used for the precondition and postcondition.) Ignoring redundancy, termination, and the trashes-clause-seq and calls-clause-seq, one can write the predicate that must be satisfied by the pre and post-states as follows, where MP is the predicate that describes the modifies clause (as defined above). 

desugar(pre-cond) => (desugar(post-cond) /\ MP)

As an example, consider the following specification. 

// @(#) $Id: set_ref_to_one.lh,v 1.5 1997/06/03 20:30:20 leavens Exp $
extern void set_to_one(int &i) throw();
//@ behavior {
//@   modifies i;
//@   ensures assigned(i, post) /\ i' = 1;
//@ }

The predicate that characterizes the relation specified for the function set_ref_to_one in the above specification is as follows. (The variable residue_i introduced by the Closure operator records whatever dependencies that may exist on i but which are not in scope; see section 11.3 of [Leino95].) 

allocated(i, pre) => (assigned(i, post) /\ (eval(i,post) = 1)
                      /\ ModifiedObjects(pre, post)
                         \subseteq ignoringTypeTags(
                                       {asTypeTaggedObject(i)}
                                       \U {asTypeTaggedObject(residue_i)}));

Because the trait function ignoringTypeTags takes off the type tag, the above can be written more simply as follows. 

allocated(i, pre) => (assigned(i, post) /\ (eval(i,post) = 1)
                      /\ ModifiedObjects(pre, post)
                            \subseteq ({widen(i)} \U {widen(residue_i)}));

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