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.
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
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)}));
Go to the first, previous, next, last section, table of contents.