Larch/C++, unlike most other specification languages,
allows you to record implementation design decisions.
(LM3, following Modula-3, also has a similar ability,
see Chapter 6 of [Guttag-Horning93] and [Jones91].)
Such detailed design decisions are recorded
by specifying private and protected members of a class.
For example, one might want to specify that the date class
was privately derived from the class fast,
if that captured some aspect of a design that could not otherwise
be specified in Larch/C++ (such as some aspect of a time budget).
Other uses for this would be making two (or more) specifications
for a class such as date;
one specification would be a normal one, specifying only the public
interface, while a refinement of this specification could be used to
specify the protected member functions.
The specification with protected members would be useful for
those programming subclasses.
See section 10.3 Specifying Protected and Private Interfaces
for a more extended discussion on this point.
Unlike very early versions of Larch/C++ [Leavens-Cheon92b], all specified class members are accessible within the specification of public (and protected and private) member functions. As in C++, protected members are accessible from within the specification of a derived class (see section 7.8 Specifying Derived Classes for details).
As a matter of style, you should specify types for which you wish to record design decisions in several layers. Doing this allows each kind of client to read a specification that is at the appropriate level of detail. For example you might first specify the public member functions so that their specifications can be used without the details of how they affect the private or protected members. Then you might specify the protected data members and any protected member functions, while at the same time giving additional details of the public member functions. Another such layer can be added for private members if desired. See section 10.3 Specifying Protected and Private Interfaces for how to use the Larch/C++ notion of refinement to do this.
Go to the first, previous, next, last section, table of contents.