In C++, declaring an object to be const
means that the (top-level) bits in the object's representation cannot change
(see section 7.1.6 of [Ellis-Stroustrup90]).
Because such an object's bit
representations cannot be changed
(at least using a path starting at the object declared const),
there can be no change in its abstract value.
That is, const-ness implies immutability.
Thus it is often an error to list as a store-ref a const object,
i.e., a term whose sort is of the form ConstObj[T].
(A notable exception to this rule is that
the traits constructed by default for structs
and classes model their instances as const objects,
see section 6.2.3 The Modifies Clause for such usage.)
For example, the following is an error, because *x has no contained
objects.
// @(#)$Id: make_zero_or_one.lh,v 1.7 1997/06/03 20:30:14 leavens Exp $
extern void make_zero_or_one(const int* x) throw();
//@ behavior {
//@ requires assigned(x, pre);
//@ modifies *x; // error!
//@ ensures (*x)' = (*x)^ \mod 2;
//@ }
Similarly in a const member function,
self should not appear in the modifies clause.
This is because in a const member function
of a class T, the sort of self is ConstObj[T],
which will usually not have any contained objects.
Recall that the notation self is short for *(this\any)
and in the specification of a const member function,
the sort of this is ConstObj[Ptr[ConstObj[T]]]
(see section 6.1.10.1 This and Self).
See Section r.9.3.1 of [Stroustrup91] for more details about const
member functions.)
One might think that the omission of const for a formal parameter
(that is an object) would provide sufficient information to make the
modifies-clause superfluous. But this is not so.
The main problem is that const-ness in C++
is only a one-level guarantee.
For example, if one of an object's data members is
a constant pointer to a mutable object
(that is, the pointer variable is const),
then the C++ guarantee of const-ness does not ensure that the abstract
value of the object does not change,
because the code could modify the object's abstract value
without changing the pointer variable.
So although it is often the case that const-ness implies no change
in abstract value, that does not always hold true.
Conversely, a change to the bits of an object
(its representation in C++ terms)
does not necessarily mean that the abstract value of the object changes.
For example, suppose rational numbers are represented by a pair of
integers, written by i/j.
Then a rational object x
whose abstract value is 1/2 might be represented by the integers
2 and 4 (2/4) and by the integers 1 and 2 (1/2).
In this case, changing the bits from 2 and 4 to 1 and 2 does not change
the abstract value.
(However, in this case, one would need to specify that the rational number
object could be modified, and that its value depends
on the two integer objects, but that its value is unchanged.
This is needed to allow the implementation described above, see [Leino95b]
and section 10.2.2 of [Leino95].
See section 7.6 The Depends Clause for details.)
So in Larch/C++ one can specify both const and modifies,
the one for C++ interfaces and the other for abstract behavior.
(Thanks to J. Horning for a personal communication on this point.)
Go to the first, previous, next, last section, table of contents.