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

7.2.2 Destructors

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 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.