We previously presented how to map implementation to specification by means of abstraction functions. We now dig into practical considerations and study how we can write such abstraction functions in a readable way, thereby making them more effective.

## Simplified Abstraction Functions

In arguably common cases, the abstraction function can be written in a simplified form, thereby increasing readability without sacrificing clarity. For instance, consider the abstraction function of a `Complex`

class whose specification does not mention any spec field (which is usually the case when the class acts as an abstraction of a well-known mathematical concept).

/** * Complex represents an immutable complex number. */ class Complex { private double real; private double imag; /* * Abstraction Function: * real + i * imag */ // ... }

In this case we write the right-hand side of the AF only. We also drop references to the representation value r as this cannot be confused with the abstract value.

## Spec field by spec field

Another simple form of abstraction function appears when the structure of the abstract value includes one or more spec fields.

/** * Segment represents an immutable line segment on a Cartesian plane. * * @specfield startPoint : Point // The starting point of the segment. * @specfield endPoint : Point // The ending point of the segment. * * @derivedfield length : real // length = sqrt((startPoint.x - endPoint.x)^2 * + (startPoint.y - endPoint.y)^2) * The straight line distance. * * @invariant length > 0 */ class Segment { private int startX; private int startY; private double length; private double angle; /* * Abstraction Function: * startPoint = (startX, startY) * endPoint.x = startX + length * cos(angle) * endPoint.y = startY + length * sin(angle) */ // ... }

In the abstraction function of `Segment`

, we still drop AF(r) as we did earlier and we simply describe how each spec field is obtained from the representation value. This takes the form of a list of equations, where the left-hand side of each equation is a spec field and the corresponding right-hand side describes how the instance variables map to this spec field.

## One-to-one mapping

It may happen that the representation of a class is so close to its specification that we find a one-to-one mapping between the spec fields and the instance variables.

/** * Segment represents an immutable line segment on a Cartesian plane. * * @specfield startPoint : Point // The starting point of the segment. * @specfield endPoint : Point // The ending point of the segment. * * @derivedfield length : real // length = sqrt((startPoint.x - endPoint.x)^2 * + (startPoint.y - endPoint.y)^2) * The straight line distance. * * @invariant length > 0 */ class Segment { private Point startPoint; private Point endPoint; /* * Abstraction Function: * startPoint = startPoint * endPoint = endPoint */ // ... }

In such an obvious case, we can drop references to the abstract value and to the representation value. Yet remember that on the left-hand side, `startPoint`

refers to a spec field, whereas on the right-hand side `startPoint`

refers to an instance variable.

These one-to-one abstraction functions may not be worth writing down. So it’s up to you to choose whether you include them or not. However keep in mind that your rep may change in the future, which can lead to a more complex abstraction function that should probably be documented.

## Recursive Abstraction Functions

Consider the following example:

/** * LinkedList represents an immutable sequence of objects. */ class LinkedList { private Object elt; private LinkedList next; ... }

We see that the representation of this class makes it of an instance of the class itself, i.e. next. Because of that, the abstract value represented by a particular instance of the class consists of (notably) the abstract value represented by next. That is, the abstraction function is recursive. To document such functions, we can rely on functional notation as in the following:

/* * Abstraction Function: * AF(r) = [] if r.elt = null * [r.elt] + AF(r.next) if r.elt != null */

In the above, the squared brackets and the “plus” sign are used to denote lists and concatenation of lists, respectively. If the instance variable `elt`

is null then the representation comes down to an empty list. Otherwise (i.e. in the recursive case), the rep defines a list whose head is `elt`

and whose tail is the result of the abstraction function on `next`

.

Abstraction functions can be written in many ways. How do / would you write yours?