Larch/C++ is the only specification language (that we know of) that allows you to specify the protected and private interfaces of a C++ class. (LM3, see Chapter 6 of [Guttag-Horning93] and [Jones91], has a similar ability with the its partial revelation mechanism that mimics Modula-3.) Specifying the protected interface documents (some of) the information needed to program and verify a derived class. Specifying a private interface documents implementation design decisions, and also specifies information needed to program and verify friend functions.
The difficulty with specifying the protected interface is that one often needs to specify exposed data members; this is nearly always a necessity when specifying the private interface. To do this one uses the idea described above (see section 7.11 Specifying Exposed Data Members).
However, most of the time a class specification is read, it will be read by clients, who are only concerned with the public interface. Hence, it is very handy to use the refinement mechanism to specify the protected interface of a class as a refinement of its public interface (see section 10.2 Class Refinement), and to specify the private interface (if at all), as a refinement of the protected interface.
If one is specifying the traits that model the class's abstract
values explicitly, then one has to provide a simulation function
(often called an abstraction function in this context [Hoare72a])
to map the abstract values of the refined specification
to those of the specification being refined.
See section 7.9.2 Inheritance with Explicitly-Given Traits and Weak Subtyping,
for an example of how to use simulation functions.
The only difference, in the case of refinement, is that
one will sometimes have to rename the sort being refined
if one is changing the set of abstract values;
to do this, one uses a refine-prefix containing
a with replace-list, where the replace-list
changes the name of the old abstract values to some other name.
For example, one might write the following.
refine MyType with OldMyType for MyType by ...
Then the trait that defines the new sort for MyType
can refer to both MyType and OldMyType.
For example, it can use both sorts to define a simulation function.
However, in most cases, it is more convenient to
use specification variables and let Larch/C++ worry about the
traits, the renaming, and the simulation function.
As an example, consider refining the specification of
the type IntSet given above (see section 10.2 Class Refinement).
Suppose we wish to implement IntSet using a private integer list
and integer data members, the_elems and the_size.
To do this,
the specification of the private interface of IntSet would be
written as follows,
starting the refinement from the specification
of the public interface in IntSet2.lcc
given above.
// @(#)$Id: IntSetPrivate.lh,v 1.16 1999/03/04 03:32:22 leavens Exp $
#include "IntSet2.lh"
#include "IntList.lh"
//@ refine IntSet
//@ by
class IntSet {
private:
IntList the_elems;
int the_size;
//@ depends value on the_elems, the_size;
//@ represents value by
//@ \A i: int (i \in value\any = i \in the_elems\any)
//@ /\ size(value\any) = the_size\any;
// Invariants documenting design decisions (rep invariants).
//@ invariant \A i: int (i \in the_elems\any
//@ => count(i, the_elems\any) = 1);
//@ invariant the_size\any = len(the_elems\any);
};
Notice that, in this refinement of IntSet,
the ghost variable value is declared to depend on
the private variables the_elems and the_size.
The relation between the specification-only variable,
value, and the_elems is given in the represents-clause
that follows the depends-clause.
It states that the_elems contains the same elements as
value, and that the value of the_size is equal to
the size of value in any visible state.
A desugared form of the above specification, is given by the following. This desugaring uses the same kind of rewriting as the desugaring for specification inheritance (see section 7.9 Inheritance of Specifications and Subtyping). In addition to copying the cases from the other parts of this specification, several redundant postconditions have been added to help make the effect of this last refinement clearer.
// @(#)$Id: IntSetPrivate2.lh,v 1.24 1999/03/04 03:32:30 leavens Exp $
#include "IntList.lh"
// from IntSet.lh
//@ spec template <class T> class Set;
//@ uses ChoiceSet(int for E, Set<int> for C), NoContainedObjects(Set<int>);
class IntSet {
private:
IntList the_elems;
int the_size;
//@ depends value on the_elems, the_size;
//@ represents value by
//@ \A i: int (i \in value\any = i \in the_elems\any)
//@ /\ size(value\any) = the_size\any;
// Invariants documenting design decisions (rep invariants).
//@ invariant \A i: int (i \in the_elems\any =>
//@ count(i, the_elems\any) = 1);
//@ invariant the_size\any = len(the_elems\any);
public:
// meaning of inherited specifications follows.
//@ spec Set<int> value;
//@ depends self on value;
IntSet() throw();
//@ behavior {
//@ constructs self; // from IntSetInformal.lh
//@ ensures informally "self' is {}";
//@ also
//@ constructs value; // from IntSet.lh
//@ ensures value' = empty;
//@ ensures redundantly the_elems' = empty /\ the_size' = 0; // by invar.
//@ }
void insert(int e) throw();
//@ behavior {
//@ modifies self; // from IntSetInformal.lh
//@ ensures informally "e is added to self";
//@ also
//@ modifies value; // from IntSet.lh
//@ ensures value' = value^ \U {e};
//@ ensures redundantly e \in the_elems'; // by the invariant
//@ }
bool is_in(int e) const throw();
//@ behavior {
//@ // from IntSetInformal.lh
//@ ensures informally "result is true just when e is a member of self";
//@ also
//@ ensures result = (e \in (value\any)); // from IntSet.lh
//@ ensures redundantly result = (e \in (the_elems\any)); // by invar.
//@ }
int pick() throw();
//@ behavior {
//@ requires informally "self is not {}"; // from IntSetInformal.lh
//@ modifies self;
//@ ensures informally "result is some member of self"
//@ "and result is also deleted from self";
//@ also
//@ requires ~isEmpty(value^); // from IntSet.lh
//@ requires redundantly ~the_size = 0; // by the invariant
//@ modifies value;
//@ ensures result \in value^ /\ not(result \in value');
//@ ensures redundantly not(result \in the_elems'); // by the invariant
//@ also
//@ requires ~isEmpty(value^); // from IntSet2.lh
//@ requires redundantly ~the_size = 0; // by the invariant
//@ modifies value;
//@ ensures result \in value^ /\ value' = delete(result, value^);
//@ }
int size() throw();
//@ behavior {
//@ ensures result = size(value\any); // from IntSet2.lh
//@ ensures redundantly result = the_size\any; // by the invariant
//@ }
};
Go to the first, previous, next, last section, table of contents.