Classes are arguably the most fundamental artifacts in object-oriented programs. They are the means of defining Abstract Data Types (ADTs), i.e. data structures with behavior that act as a simplification of domain concepts within the program to be.

Of course, the class has not to deal with all the complexity of its corresponding domain concept; it is merely an abstraction of this concept. In the same vein, **understanding the purpose of a class should not require a thorough knowledge of its inner working.**

As for methods, one should first focus on **what** a class should do (i.e. its specification) and then **how** it does it (i.e. its implementation). This way of designing classes favors their correct use and lead to an increase of code quality and maintainability.

## Abstract Value and Specification Fields

When a programmer has to introduce a new concept within a program, she can often reduce this concept to a simplified form; the whole complexity of the concept may indeed not be needed, or may even be impossible to encode in the program. Thus, the programmer thinks this concept in terms of a few *fields* that represent it.

Consider, e.g., a segment of line in a Cartesian plane. Fundamentally, this segment consists of an uncountable number of points. Yet it is often sufficient to know only the coordinates of its two extremities. These constitute the **abstract value** of the segment, i.e. the way we want to view the Segment ADT (or abstract type), as clients of the type.

One commonly defines the abstract value in terms of its constituent **specification fields** (or “spec fields”). These can be used in specifications to reference particular elements of the abstract value concisely and without ambiguity.

For each spec field, one often finds a corresponding observer method that returns the value of this spec field, although this is not always the case. Likewise, the implementation of the class may include a proper instance variable that corresponds to a given spec field (for simplicity, consider for now that instance variables are the non-static attributes of the class). The value of the spec field can indeed be derived from multiple instance variables. In some cases it may not be available at all.

In our specification syntax, we propose to list spec fields in the overview section of the class using the tag **@specfield**, followed by the name of the spec field, then its type, and finally a short description. For example, the abstract value of our class `Segment`

is composed of two spec fields, `startPoint`

and `endpoint`

, which we document as follows:

/** * Segment represents a mutable line segment on a Cartesian plane. * * @specfield startPoint : Point // The start point of the segment. * @specfield endPoint : Point // The end point of the segment. */

We can specify the class `Point`

in a similar fashion:

/** * Point represents an immutable point on a Cartesian plane. * * @specfield x : real // The abscissa of the point. * @specfield y : real // The ordinate of the point. */

By convention lowercased type names like *real* or *set* refer to usual mathematical concepts, whereas uppercased names refer to other ADTs / classes. When possible, prefer the use of a mathematical concept to an ADT, as it allows you to hide the concrete type in your specification, and thus to change it in your implementation without modifying the specification. For example, write `real`

rather than `Double`

or `BigDecimal`

.

## Derived Specification Fields

Derived specification fields (or **derived fields**) are relevant information related to the abstract value that can be derived from spec fields. The purpose of derived fields is to simplify specifications that refer to spec fields in a non-trivial way. For example, the length of a segment can be derived from its start point and end point. We document derived fields similarly to spec fields, using the appropriate tag **@derivedfield**.

/** * Segment represents a mutable line segment on a Cartesian plane. * * @specfield startPoint : Point // The start point of the segment. * @specfield endPoint : Point // The end point of the segment. * * @derivedfield length : real // length = sqrt((startPoint.x - endPoint.x)^2 * + (startPoint.y - endPoint.y)^2) * The distance between startPoint and endPoint. */

In the above, the derived field `length`

is specified w.r.t. the spec fields `startPoint`

and `endPoint`

.

The documentation of derived fields must always explain how its value is derived from other spec fields. They can then be used for convenience in other parts of the specification. It is indeed easier to read and write `length`

than `sqrt((startPoint.x - endPoint.x)^2 + ...)`

each and every time we use it.

## Abstract Invariants

It often occurs that some (combinations of) spec field values are illicit. The set of licit values should be documented in **abstract invariants**, i.e. conditions over the abstract value that any implementation of the class must guarantee to hold. The invariants are typically specified in terms of spec fields and derived fields. For instance, the length of the segment must be greater than zero, or equivalently the start point of the segment must be different from its end point. In the overview of the class, we use the tag **@invariant** to document abstract invariants.

/** * Segment represents a mutable line segment on a Cartesian plane. * * @specfield startPoint : Point // The start point of the segment. * @specfield endPoint : Point // The end point of the segment. * * @derivedfield length : real // length = sqrt((startPoint.x - endPoint.x)^2 * + (startPoint.y - endPoint.y)^2) * The distance between startPoint and endPoint. * * @invariant length > 0 */

## Method Specifications

In our previous post, we explained how to specify standalone methods. Within a class, methods may have **pre** and **post** over the abstract value (and thus over the spec and derived fields) of the current instance and the other ADTs used as input parameters.

We now analyze the specification of a few methods of class `Segment`

. Let us begin by the constructor.

/** * @requires startPoint != null && endPoint != null && startPoint != endPoint * @effects Makes this be a new Segment s, with s.startPoint = startPoint * and s.endPoint = endPoint. */ Segment(Point startPoint, Point endPoint)

The @effects clause of the constructor must mention how all the spec fields are initialized. However, the derived field (in this case, `length`

) hasn’t to be mentioned since it is determined from `startPoint`

and `endPoint`

. More generally, derived fields never appear in the @effects clause of any method.

/** * @requires startPoint != null && startPoint != this.endPoint * @modifies this * @effects Sets this.startPoint to startPoint */ void setStartPoint(Point startPoint)

The above method changes the start point of the current instance. The @modifies clause indicates that the instance may be modified, and the @effects clause states how it (i.e. which spec field) is modified. Note that the @requires clause, in addition to a typical non-null parameter precondition, also supports the abstract invariant by excluding that the new start point be equal to the current end point.

/** * @requires segment != null * @return this.length - segment.length, i.e., the difference in length * between this and segment. */ double differenceInLength(Segment segment)

The `differenceInLength`

method uses the derived field `length`

of the current instance as well as that of the segment parameter. Note that this specification would be way longer if the derived field hadn’t been introduced in the overview of the class.

Now tell us about how do you document classes? Do you make any distinction between the abstract value of your class and its implementation?

Pingback: Mapping implementation to abstraction | The Conscious Programmer()

Pingback: 6 tips to write representation invariants | The Conscious Programmer()