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

6.2 Mutation

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 void function has a result, which is theVoid. See section 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 allocated and assigned, 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.