To specify a function that mutates objects, the specification must include a modifies-clause. The absence of a modifies-clause means that no objects can have their abstract values mutated by an execution of the function (that satisfies the pre-condition). The presence of a modifies-clause asserts that only the set of objects described, may have their abstract values newly-defined or changed by the function. We say that an object is described by a modifies-clause if it is either explicitly specified by it or if some described object depends on it (see Chapter 10 of [Leino95]). (See section 7.6 The Depends Clause for a description of dependencies.) This is a strong indirect assertion that no other allocated objects, other than those described, are allowed to change their abstract values. An object that is included in the set described by the modifies-clause does not have to be changed by the function; the point is that it is allowed to be changed.
modifies-clause-seq ::= modifies-clause [ modifies-clause ] ... modifies-clause ::=modifies[redundantly] store-ref-list;|constructs[redundantly] store-ref-list;store-ref-list ::= store-ref [,store-ref ] ... |nothing|everythingstore-ref ::= term |reach(term)
See section 6.9.4 Redundancy in Frames for
the meaning of redundantly used in a modifies-clause.
When several non-redundant modifies-clauses are listed in
a modifies-clause-seq, this is the same as listing each of their
store-ref-lists in a single modifies-clause.
If more than one non-redundant modifies-clause is given,
then none of the store-ref-lists may be of the form
nothing or everything.
Because it is possible to translate multiple non-redundant
modifies-clauses into a single modifies-clause,
we will assume from now on that there is only one
non-redundant modifies-clause.
As an example,
(assuming that there are no dependencies visible)
the function swap specified below may change the abstract values
of both x
and y, but nothing else; i.e., it cannot change
the abstract values of any other global variables.
// @(#)$Id: swap.lh,v 1.5 1997/06/03 20:30:22 leavens Exp $
extern void swap(int& x, int& y) throw();
//@ behavior {
//@ requires assigned(x, pre) /\ assigned(y, pre);
//@ modifies x, y;
//@ ensures x' = y^ /\ y' = x^;
//@ }
Unlike earlier versions of Larch/C++ (and LCL), mutation of an object does not include deallocation or "trashing" it. (The current semantics is based the work of Chalin [Chalin95].) The modifies-clause only concerns objects that:
It says that out of all such objects, only the objects described by the modifies-clause may have their abstract values changed.
The modifies clause thus does not concern objects that are:
freshly allocated by the function
(i.e., that are not allocated in the pre-state
and allocated in the post-state),
deallocated by the function
(allocated in the pre-state and not allocated in the post-state),
or
not assigned in the post-state.
The reason the modifies-clause does not concern objects x
that are not assigned in the post-state
(i.e., such that ~assigned(x, post))
is because the abstract values of such objects are not well-defined.
For such an unassigned object, there is no good way to define
the concept of mutation.
This is also the reason that the modifies clause is not concerned with
objects that were not allocated in the pre-state.
(Technically, this is because state functions will map such objects
to arbitrary values,
and there is no guarantee that the pre-state did not map such an object
to the same arbitrary value as the post-state.(4))
Allocation of objects can be specified by using the keyword fresh
(see section 6.3.1 Fresh).
Trashing objects (either by making them unassigned or by deallocating them)
is only permitted if a function is specified
using a trashes-clause (see section 6.3.2 The Trashes Clause).
This means that all objects not described by the trashes-clause-seq
(and for an omitted trashes-clause-seq this is literally all objects)
that are allocated in the pre-state remain allocated in the post-state.
Furthermore, all objects not described by the trashes-clause-seq
that were assigned in the pre-state remain assigned in the post-state.
An omitted modifies-clause-seq is equivalent to
a modifies-clause-seq of the form modifies nothing;
meaning no (already assigned) object can be mutated by the specified function.
The other extreme is modifies everything; meaning the function can
change all objects to which it has access in the pre-state.
Thus, modifies everything means that the frame axiom
is trivially satisfied.
A modifies clause may be written informally.
See section 6.1.4 Informal Descriptions for the syntax;
in this case the clause should informally describe a set of (typed) objects.
However,
you should avoid using informality in the modifies-clause if possible,
as it is easy, by naming formal parameters,
or by using everything or reach,
to specify something formal.
The clause modifies reach(x); means that the function may change
the abstract values of
the set of objects that are reachable from x,
including x itself (see section 6.2.3.5 Reach).
A simple example of using a term in a modifies-clause is
given by the following.
In this example, the store-ref-list *p
could also be written as p[p.idx].
See section 11.8 Pointer Types for details on these alternatives to writing *p
and for the trait function allocated used in the precondition.
// @(#) $Id: set_to_one.lh,v 1.10 1998/08/27 22:56:52 leavens Exp $
extern void set_to_one(int *p) throw();
//@ behavior {
//@ requires allocated(p, pre);
//@ modifies *p;
//@ ensures assigned(p, post) /\ (*p)' = 1;
//@ ensures redundantly assigned(*p, post);
//@ }
The reason the post-condition asserts that assigned(p, post)
is that p is not required to point at an assigned object in the
pre-state. As stated in the redundant ensures-clause
(see section 6.9.3 Redundant Ensures Clauses or Claims)
it follows that assigned(*p, post) holds
(See section 11.8 Pointer Types for details on the meaning of assigned).
This makes it clear when *p is assigned.
(Technically, the conjunct assigned(p, post) or
assigned(*p, post) is needed in the post-condition
because otherwise *p will not have a well-defined value
in the post-state.)
One should be careful, however, with pointers and arrays,
to ensure that one gives the correct set of objects.
The trait function contained_objects,
is useful in this respect.
For pointers into arrays (such as array formal parameters)
and for arrays, one can use trait functions
such as objectsInRange found in the traits
for pointers (see section 11.8 Pointer Types for details in the trait Pointer)
and arrays (see section 11.7 Array Types for details in the trait Array).
For string manipulations, one can use a more specialized trait function,
such as objectsToNull (see section 11.9 Character Strings for details of
the trait cpp_char_string).
An example of the use of objectsToNull is given below.
(See section 6.9.3 Redundant Ensures Clauses or Claims for the meaning
of the redundant ensures-clause.)
// @(#) $Id: poorly_encrypt.lh,v 1.11 1998/08/27 22:56:51 leavens Exp $
extern void poorly_encrypt(unsigned char *s) throw();
//@ behavior {
//@ uses cpp_unsignedChar_string;
//@ requires nullTerminated(s, pre);
//@ modifies objectsToNull(s, pre);
//@ ensures \A i: int (legalStringIndex(s,pre,i)
//@ => (*(s + i))' = (*(s + i))^ + 1);
//@ ensures redundantly (legalStringIndex(s,pre,0) /\ (*s)^ = UCHAR_MAX)
//@ => ((*s)' = 0);
//@ }
Further discussion of topics related to modifies-clause is found below.
Go to the first, previous, next, last section, table of contents.