In C++, a destructor is a member function
whose name is written with a twiddle (~)
preceding the name of the class it appears in.
For example, the destructor for class Person is named ~Person.
In C++, a destructor's main responsibility is to deallocate objects
that the constructor (or other member functions)
may have dynamically allocated
(see section 12.4 of [Ellis-Stroustrup90]).
Since such allocations are usually invisible to clients,
the deallocations are also usually of no concern to clients.
Thus the typical destructor specification merely says that
calling the destructor modifies nothing and terminates.
This can be written with the following spec-case.
ensures true;
Cases where one would want to say more in a destructor
include cases where the data members
are exposed (see section 7.11 Specifying Exposed Data Members),
or cases where the class is being used as a repository of storage,
which will all be deleted at the same time.
In such cases, one might write a spec-case like
the following.
This says that the object may be modified
and that the directly reachable objects in the object should
not be reused after the call.
(See section 6.3.2.1 Trashed for the meaning of trashed.)
modifies self; trashes contained_objects(self^, pre); ensures trashed(contained_objects(self^, pre));
[[[Need a real example.]]]
A destructor may not be declared const
(see section 9.3.1 of [Ellis-Stroustrup90]).
Because the C++ delete operator actually trashes an instance,
not the destructor,
in the specification of a destructor
it is only necessary to list the object
self in the modifies-clause
if the destructor changes the abstract value
(for example, by trashing exposed data members that are parts of the
abstract value).
(See section 6.2.3 The Modifies Clause for details on the modifies-clause.
See section 6.3.2 The Trashes Clause for details on the trashes-clause.)
As in C++ (see section 12.4 of [Ellis-Stroustrup90]), no return type can be specified for a destructor. A class can specify at most one destructor, which is not inherited.
In contrast to constructors, one can, and one often should,
specify a destructor as virtual.
Ellis and Stroustrup recommend making the destructor virtual
whenever there is at least one other virtual function
(page 278 of [Ellis-Stroustrup90]).
See section 7.2.3 Implicitly Generated Member Specifications for the meaning of a class specification with no destructor declared.
Go to the first, previous, next, last section, table of contents.