In C++, a constructor is a member function with the same name
as the class it appears in.
For example, a constructor for class Person is named Person.
A class can specify several constructors.
In C++, the compiler takes care of allocating storage for instances
of classes (see section 12.6 of [Ellis-Stroustrup90]).
So the job of a constructor is simply to initialize the newly created instance.
That is, the constructor really modifies the abstract value of the instance,
from an undefined initial value to the value desired.
Thus by the semantics of Larch/C++, one has to state that self
is modified in the modifies-clause.
Thus, the typical modifies-clause in a constructor looks like
the following (or something equivalent, see below).
modifies self;
(Hence it is not usually sensible for the constructor to be specified as
a const member function.)
However, since clients of a class need not be interested
in such detail,
in Larch/C++ one can use constructs instead of modifies
in a modifies-clause.
That is, one can write the following.
constructs self;
This does not affect the meaning of the modifies-clause,
the same implementations satisfy the specification,
but it gives an impression to readers that is more connotative.
An example is given in the specification of Money
above (see section 7.1.2 A Design with a Nontrivial Trait (Money)).
See section 6.2.3 The Modifies Clause for the syntax of the modifies-clause.
In C++, a constructor for a class has the same name as the class itself. There can be several constructors for each class, as long as they differ in their parameter types (see chapter 13 of [Ellis-Stroustrup90]).
It is often useful to specify constructors with default parameter values,
as in the specifications of Money and BoundedIntStack
(see section 7.1 Examples of Class Specifications).
See section 6.6 Default Arguments for details on how to do this.
A constructor that can be called with no parameters
is called a default constructor
(section 12.1 [Ellis-Stroustrup90]).
A class without a default constructor
(such as Person in section 7.1.1 A First Class Design (Person))
cannot be used as an element of an array.
Thus, as a general rule, one should try to specify a default constructor
for each class.
For the class Person,
it is not obvious what the name should be by default.
One possibility for the default constructor of the class Person
is as follows.
However, such a specification is not completely satisfactory,
because it is not clear that the "default" person should have age 0.
(The term uptoNull("J. Doe",any) has sort String[char],
and uptoNull is used to convert the C++ string constant,
of sort Arr[Obj[char]] to that sort.)
Person();
//@ behavior {
//@ constructs name, age;
//@ ensures name' = uptoNull("J. Doe",any) /\ age' = 0;
//@ }
Although Larch/C++ will provide an implicit specification of the default constructor if you do not specify any constructors for a non-abstract class (see section 7.2.3 Implicitly Generated Member Specifications), doing so is usually a bad idea, because the implicit specification does not tell the user much. As a rule, you should always specify at least one constructor for each concrete class.
As in C++ (see section 12.6 of [Ellis-Stroustrup90]),
no return type can be specified for a constructor.
Furthermore, a constructor cannot be specified as virtual
(but see section 6.7.1 of [Stroustrup91]).
As in C++, constructors and their specifications are not inherited.
[[[Need example of constructor that has an exposed data member and allocates storage for it dynamically.]]]
A constructor in a class T is a copy constructor
if the type of its first (leftmost) parameter is const T&
or T&,
and if all its other parameters have defaults
(see section 6.6 Default Arguments).
As in C++, a constructor in a class T
cannot have just one parameter of type T.
See section 7.2.3 Implicitly Generated Member Specifications for the meaning of a class specification that does not declare any copy constructors.
Go to the first, previous, next, last section, table of contents.