6.2 Mutation

Mutation of an object means changing its abstract value. This can happen in one of two ways:

• the object had a well-defined abstract value that is changed, or
• the object had no well-defined abstract value, but it became well-defined.

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:

• the pre-state, which maps objects to their values just before the function body is run, but after parameter passing, and
• the post-state, which maps objects to their values at the point of returning from the call (or throwing an exception), but before the function parameters go out of scope.

Thus, to allow for mutation, the formal model of a C++ function (that cannot throw exceptions) is as a relation between:

• the formal arguments and the pre-state, and
• the post-state and the result.

Note that the in Larch/C++ even a void function has a result, which is theVoid. See section 6.1.10.2 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.

• State Functions
• Allocated and Assigned
• The Modifies Clause

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