Mutation of an object means changing its abstract value. This can happen in one of two ways:
The word "modifies" is sometimes used as a synonym for "mutates".
To specify a function that mutates an object,
one usually has to refer to the object's abstract value
in two states:
just before the function body is run (but after parameter passing)
and just as it is about to return.
Informally one refers to the value of an object at a given time as its state.
More formally, a state is a (mathematical) function from objects
to their values.
An informal phrase such as "the object
x has value 2 before the call"
means that the state before the call (after parameter passing)
maps the object
x to 2.
See section 2.8 Objects and Values for an introductory discussion of objects and values.
The states of interest in a function specification are as follows:
Thus, to allow for mutation, the formal model of a C++ function (that cannot throw exceptions) is as a relation between:
Note that the in Larch/C++ even a
has a result, which is
See section 188.8.131.52 Result for more discussion on this point.
Therefore a function specification's precondition describes the arguments and pre-states over which the function is defined (the domain of the relation). The postcondition describes the relation itself; that is, it describes the set of post-state and result pairs that are related to a given tuple of actual arguments and a pre-state.
The modifies-clause in a specification can be used to state what objects a function is allowed to mutate, and what objects it is not allowed to mutate. (It is part of a "frame axiom" for a specification [Borgida-etal95]. The other part of the frame axiom is the trashes-clause, which, if omitted, says that no object can become unassigned or deallocated (see section 6.3.2 The Trashes Clause).
The subsections below describe:
state functions, which allow one to specify the value of an object in
the pre- or post-state,
the trait functions
which allow one to specify whether objects are allocated and well-defined,
the modifies-clause, and
formal details of the modifies-clause.
Go to the first, previous, next, last section, table of contents.