7.11 Specifying Exposed Data Members

In C++, nothing stops you from having public data members in a class. Indeed, as typically used, a C++ struct is like a class with public data members and few, if any, member functions. However, since one of the main reasons for using classes is to hide how data is represented, one should think twice before specifying public data members in a class. Nevertheless, there may be situations in public, or as we will call them in this section, exposed data members are useful.

To take a simple example, suppose we are writing a programming language interpreter, and need a class to represent integer variables (in the language being interpreted). Objects of this class will have a name and an integer variable cell. To avoid duplicating the functionality of C++ integer variables (and to provide an example for this section), suppose we choose to expose the integer variable in the implementation. That is, suppose we decide that the C++ class implementing this type will look like the following.

class IntVar {
public:
  int var;
  // ...
};

This is very easy to specify in this form, since as the exposed data member serves the same role as a specification variable would normally. Thus, there is no problem, as long as you are willing to allow Larch/C++ to automatically construct a trait for the abstract model. (If you want to build your own trait, you can model it on the ones automatically constructed by Larch/C++. See section 11.10 Structure and Class Types for details.)

The interface specification given below has only a constructor (with two default parameters) and a member function name. (Although Larch/C++ considers string literals to be arrays of characters, a pointer argument such as this can be initialized from such an array, and so the specification does not have a sort error.)

// @(#)$Id: IntVar.lh,v 1.14 1997/07/31 03:10:16 leavens Exp $

#include "AbstractString.lh"

//@ uses cpp_const_char_string;

class IntVar {
public:
  int var;
  //@ spec String<char> its_name;
  //@ constraint its_name^ = its_name';  // the name can't be changed

  IntVar(const char vname[] = "unnamed", int initial_value = 0) throw();
  //@ behavior {
  //@   requires nullTerminated(vname, any);
  //@   constructs var, its_name;
  //@   ensures its_name' = throughNull(vname, any)
  //@        /\ var' = initial_value;
  //@ }

  const char * name() const throw();
  //@ behavior {
  //@   ensures nullTerminated(result, post)
  //@           /\ throughNull(result, post) = its_name\any;
  //@ }
};

A final note about this example. Just because it is necessary to expose one data member, does not mean that one needs to expose them all. In the IntVar example, the data member its_name is a specification variable, and hence cannot be used by C++ clients.

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