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

7.2.3 Implicitly Generated Member Specifications

C++ implicitly defines several member functions for the user if they are not explicitly defined (section 12.3c of [Ellis-Stroustrup90]). Implicitly defined member functions are public. If the C++ member function is implicitly defined, and if the class is not abstract, then Larch/C++ implicitly provides an appropriate specification. C++ implicitly generates member functions in the following cases.

The interfaces for these member functions are given in the following. 

// @(#)$Id: default_interfaces.lh,v 1.2 1997/01/10 23:49:22 leavens Exp $

class T {
public:
  // default interfaces for member functions when not explicitly declared.
  T() throw();                            // constructor
  T(const T& arg) throw();                // copy constructor
  ~T() throw();                           // destructor
  T& operator = (const T& from) throw();  // assignment operator
};

As a general rule, the default specifications generated by Larch/C++ are sensible and useful. However, it is probably not a good idea to leave the specification of the default constructor to Larch/C++. Furthermore, if one specifies a class with virtual member functions, then one probably wants a virtual destructor, but the destructor implicitly generated by C++ is not virtual. Thus, for a class with virtual member functions, it is best to explicitly specify a virtual destructor.

The following describe the implicit specifications generated by Larch/C++. No specifications are implicitly generated for abstract classes.

Consider the specification of a class T. Then the default constructor specification, when implicitly generated is as follows. The specification just says that only the object self can be modified, nothing about the abstract value of self is guaranteed, except that it is assigned and that its immediate subobjects (e.g., specification variables) are assigned. 

// @(#)$Id: default_constructor.lh,v 1.3 1998/08/27 22:56:49 leavens Exp $
#include "default_interfaces.lh"

T::T() throw();
//@ behavior {
//@   constructs self;
//@   ensures true;
//@   ensures redundantly assigned(self, post) /\ assigned(self', post); 
//@ }

The implicitly-generated destructor specification, when needed, is the following. The specification says that calls to the destructor are guaranteed to terminate, and the destructor may not change any objects. Hence the default destructor does nothing. (Recall that it is the C++ delete operator that actually trashes a class instance, not the destructor.) Note that the implicitly generated destructor is not virtual; thus if you have virtual function members in a class, you probably should declare a destructor explicitly. 

// @(#)$Id: default_destructor.lh,v 1.1 1997/01/10 23:57:29 leavens Exp $
#include "default_interfaces.lh"

T::~T() throw();
//@ behavior {
//@   ensures true;
//@ }

The implicitly-generated copy constructor specification, when needed, is the following. The specification says that the value of the abstract value of the constructed object, self", is the same as the value of the argument's abstract value, arg\any\any. This corresponds to the code that C++ generates for hte default copy constructor, which copies the values from each data member of arg to the corresponding data member of self. (See section 6.2.2 Allocated and Assigned for the trait function assigned used in the pre-condition.) 

// @(#)$Id: default_copy_ctor.lh,v 1.3 1998/08/27 22:56:50 leavens Exp $
#include "default_interfaces.lh"

T::T(const T& arg) throw();
//@ behavior {
//@   requires assigned(arg, any) /\ assigned(arg\any, any);
//@   constructs self;
//@   ensures self" = arg\any\any;
//@   ensures redundantly assigned(self, post);
//@ }

The implicitly-generated assignment operator specification, when needed, is the following. The specification says that the result is the object being assigned (self), and that the value of the abstract value of self in the post-state self" is the same as the value of the abstract value of the argument from. 

// @(#)$Id: default_assignment_op.lh,v 1.3 1998/08/27 22:42:13 leavens Exp $
#include "default_interfaces.lh"

T& T::operator = (const T& from) throw();
//@ behavior {
//@   requires assigned(from, any) /\ assigned(from\any, any);
//@   modifies self;
//@   ensures result = self /\ self" = from\any\any;
//@   ensures redundantly assigned(self, post) /\ assigned(self', post);
//           thus
//@   ensures redundantly assigned(result, post) /\ assigned(result', post);
//@ }

As an example, the type Person specified above (see section 7.1.1 A First Class Design (Person)) has both a constructor and a destructor specified, so no constructor or destructor is implicitly generated. The destructor is specified because there are virtual member functions, and thus the implicitly generated non-virtual destructor would not be quite right. In Person, there is no copy constructor or assignment operator specified, so implicitly the following public member specifications are implicitly added to the specification of Person by Larch/C++. (See section 10 Refinement for a discussion of this kind of refinement specification.) 

// @(#)$Id: Person_defaults.lh,v 1.7 1999/03/03 19:11:51 leavens Exp $

#include "Person.lh"

//@ refine Person by
//@ class Person {
//@ public:     // implicit specifications added to class Person

  //@ spec Person(const Person& arg) throw();
  //@ behavior {
  //@   requires assigned(arg, any) /\ assigned(arg\any, any);
  //@   requires redundantly assigned(arg\any.name, any)
  //@                       /\ assigned(arg\any.age);
  //@   constructs self;
  //@   ensures self" = arg\any\any;
  //@   ensures redundantly name' = arg\any.name\any
  //@                    /\ age' = arg\any.age\any;
  //@ }
  
  //@ spec Person& operator = (const Person& from) throw();
  //@ behavior {
  //@   requires assigned(from, any) /\ assigned(from\any, any);
  //@   requires redundantly assigned(from\any.name, any)
  //@                        /\ assigned(from\any.age);
  //@   modifies self;
  //@   ensures result = self /\ self" = from\any\any;
  //@   ensures redundantly name' = arg\any.name\any
  //@                       /\ age' = arg\any.age\any;
  //@ }
//@ };

The above specifications are written using self, instead of the two specification variables name and age. Thus, one has to look at the automatically-constructed trait Person_Trait (see section 7.1.1 A First Class Design (Person)) and recall that self" means eval(eval(self, post), post) (see section 6.2.1 State Functions) to understand it. The idea is that eval(self, post) is a tuple of objects, containing objects that represent the specification variables age and name. These objects will generally differ, and so what is really desired is that the values within these objects are the same in the post-state. This explains the second evaluation, which returns a tuple of values. A more readable form of the default specification's meaning for the pre- and postconditions can be seen by looking at the redundant requires-clause and ensures-clause of each specification.

The class Money specified above (see section 7.1.2 A Design with a Nontrivial Trait (Money)) also does not have a copy constructor or assignment operator specified, so these are also implicitly specified by Larch/C++, as with the class Person. The second-layer of eval and assigned functions, which work on Money values, are defined in the trait PureValue(Money), which is included in the trait NoContainedObjects(Money) (see section 7.5 Contained Objects for details).

If one wishes to not have give clients access to one of these implicitly generated member functions, one has to, as in C++, declare it as protected or private. For example, it might be useful to specify the copy constructor and assignment operator as private, if one wishes to prevent copies of objects of the type from being made.

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