10.2 Class Refinement

Class refinement allows one to strengthen a class specification, by possibly changing the abstract model and adding additional cases to the member function specifications. One use of refinement is to increase the formality of a specification; that is, one can refine an informal specification by a formal one. Another use of refinement is to specify the protected or private interface of a class, by refining a specification of its public interface. (See section 10.3 Specifying Protected and Private Interfaces for examples of how that is done.)

Refinement works by the same mechanism as specification inheritance (see section 7.9 Inheritance of Specifications and Subtyping), but unlike subtyping, refinement also applies to constructors and non-virtual member functions. Also, with refinement, both the refined and the refining classes must have the same name. Because the classes may have the same name, it is possible to use the same set of abstract values for each.

The interface of the refinement may have more members than the class it refines. This is useful, for example, when exposing details about protected and/or private members in the refinement. Furthermore, the interface of a member function in the refinement may allow fewer exceptions to be thrown than in the refined specification. For example the refinement may give an exception-decl when none was given originally (see section 6.11 Exceptions). (Recall that in C++, not giving an exception-decl allows all exceptions to be thrown.)

As an example of refinement, consider the following informal specification of a class IntSet. Note that although informal descriptions are used, the modifies-clause is easily made formal in each function.

// @(#)$Id: IntSetInformal.lh,v 1.13 1997/08/05 23:06:08 leavens Exp $

class IntSet {
public:
  IntSet() throw();
  //@ behavior {
  //@   constructs self;
  //@   ensures informally "self' is {}";
  //@ }

  void insert(int e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures informally "e is added to self";
  //@ }

  bool is_in(int e) const throw();
  //@ behavior {
  //@   ensures informally "result is true just when e is a member of self";
  //@ }

  int pick() throw();
  //@ behavior {
  //@   requires informally "self is not {}";
  //@   modifies self;
  //@   ensures informally "result is some member of self"
  //@                      "and result is also deleted from self";
  //@ }
};

The above specification is refined by the following. Note that since all of the function specifications that would be inherited were specified informally above, each function is respecified below. The trait, ChoiceSet used to specify the abstract values of the specification-only class Set<int> is found on page 176 of [Guttag-Horning93].

// @(#)$Id: IntSet.lh,v 1.15 1999/03/02 17:56:26 leavens Exp $

#include "IntSetInformal.lh"

//@ spec template <class T> class Set;
//@ uses ChoiceSet(int for E, Set<int> for C), NoContainedObjects(Set<int>);

//@ refine IntSet
//@ by
class IntSet {
public:
  //@ spec Set<int> value;
  //@ depends self on value;
  //@ represents self by self\any = value\any;

  IntSet() throw();
  //@ behavior {
  //@   constructs value;
  //@   ensures value' = empty;
  //@ }

  void insert(int e) throw();
  //@ behavior {
  //@   modifies value;
  //@   ensures value' = value^ \U {e};
  //@ }

  bool is_in(int e) const throw();
  //@ behavior {
  //@   ensures result = (e \in (value\any));
  //@ }

  int pick() throw();
  //@ behavior {
  //@   requires ~isEmpty(value^);
  //@   modifies value;
  //@   ensures result \in value^ /\ not(result \in value');
  //@ }
};

Notice the depends-clause in the specification above. This is needed to allow the data member value to be modified, when the informal specification allows only self to be modified.

The represents-clause in the above specification says that, the abstract value of self in any state is the same as the value of value in that state.

The specification of pick above is somewhat loose, in that it does not require only the result to be deleted from the post-state value of self. We can correct this oversight by an additional refinement, shown below. The refinement also limits the exceptions that can be thrown by pick and specifies an additional member function size.

// @(#)$Id: IntSet2.lh,v 1.12 1997/07/31 18:19:03 leavens Exp $

#include "IntSet.lh"

//@ refine IntSet
//@ by
class IntSet {
public:
  int pick() throw();
  //@ behavior {
  //@   requires ~isEmpty(value^);
  //@   modifies value;
  //@   ensures result \in value^ /\ value' = delete(result, value^);
  //@ }

  int size() throw();
  //@ behavior {
  //@   ensures result = size(value\any);
  //@ }
};

This second refinement of IntSet uses the same set of specification variables (and hence abstract values) as the first.

When making a refinement that exposes more information about a type, for example, when adding operations of the protected or private interface, it is useful to change the set of abstract values. See section 10.3 Specifying Protected and Private Interfaces for an example. However, before seeing how to do that, it may be useful to review at how exposed data members can be specified (see section 7.11 Specifying Exposed Data Members), since they are common in protected and private specifications.

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