#### 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.

• TTO(SR) = SR, if the sort of SR is `Set[TypeTagggedObject]` (this includes the case when SR has the form `reach(term)`: see section 6.2.3.5 Reach for the details in this case), and
• TTO(SR) = `contained_objects(SR, pre)`, otherwise.

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)}));
```