6.170 / Spring 2004 / Writing Abstraction Functions & Rep Invariants

Handout S8

• Introduction
• Abstraction Functions
  • Where Are R and A Defined?
  • AF(r)
  • Mathematical Abstract Values
  • Specification Fields
  • Using Spec Fields for Specifications
• Rep Invariants
  • Choosing the Rep Invariant
  • Checking the Rep Invariant at Runtime
• A Complete Example
• General Hints on Readability

Introduction

Abstraction Functions

public class Complex {
  private double real;
  private double imag;
  ...
}

Where Are R and A Defined?

/**
 * Complex represents an immutable complex number.    <=== this is A
 */
public class Complex {
  private double real;    <=== these fields form R
  private double imag;
  ...
}

AF(r)

/**
 * Complex represents an immutable complex number.
 */
public class Complex {
  private double real;
  private double imag;

  // The abstraction function is 
  //      AF(r) = r.real + i * r.imag
  ...
}

/**
 * Cons represents an immutable sequence of objects.
 */
public class Cons {
  private Object car;
  private Cons cdr;

  // The abstraction function is 
  //      AF(r) = [] if r = null
  //              [r.car] : AF(r.cdr) if r != null
  ...
}

/**
 * Complex represents an immutable complex number.
 */
public class Complex {
  private double real;
  private double imag;

  // The abstraction function is 
  //      real + i * imag
  ...
}

Mathematical Abstract Values

• a set of integers
• a sequence of characters (i.e., a string)
  
• a pair of real numbers (or a triple, or in general a tuple)

• set comprehension: { x | P(x) } denotes the set of all elements x that satisfy the property P. More generally, { f(x) | P(x) } denotes the set of values of the expression f(x) for all x that satisfy the property P.
  
• set union:  x U y denotes the union of two sets x and y.  (This can also be written x + y when there's no danger of confusion with addition.)
• set membership: a in x tests whether a is an element of the set x.
  
• sequence construction: [a, b, c] denotes a sequence of three elements.
• sequence concatenation:   x : y denotes the concatenation of two sequences x and y.  (This can also be written x ^ y or x + y when there's no danger of confusion with exponentiation or addition.)
• sequence indexing: x[i] denotes the ith element of a sequence x.
  
• set or sequence size:  |x| denotes the number of elements in a set or sequence x.
  
• tuple construction: <a, b, c> is a tuple of three elements.  This is also written (a, b, c).  Unlike sequences, tuples are fixed-length, so we don't normally think about concatenating them.

Specification Fields

/**
 * Line represents an immutable line segment in the plane.
 * @specfield start : Point // start point
 * @specfield end : Point   // end point
 */

By convention, in specification fields, lowercase types like sequence or set refer to mathematical entities. Capitalized types refer to other ADTs (i.e., Java classes).  Where you have a choice, prefer a mathematical entity as the type of a spec field; better to use sequence than List, for example.  It's more elegant, and reduces the coupling between your specification and concrete Java classes.

public class Line {
    private Point start;
    private Point end;

    // Abstraction function is
    //    AF(r) = line l such that
    //       l.start = r.start
    //       l.end = r.end
    ...
}

public class Line {
    private Point start;
    private double length;
    private double angle;

    // Abstraction function is
    //    AF(r) = line l such that
    //       l.start = r.start
    //       l.end.x = r.start.x + r.length * cos(r.angle)
    //       l.end.y = r.start.y + r.length * sin(r.angle)
    ...
}

    // Abstraction function is
    //       start = start
    //       end.x = start.x + length * cos(angle)
    //       end.y = start.y + length * sin(angle))

/**
 * Card represents an immutable playing card.
 * @specfield suit : {Clubs,Diamonds,Hearts,Spades} // card suit
 * @specfield value : {Ace,2,...,10,Jack,Queen,King} // card rank
 */

public class Card {
    private int index;

    // Abstraction function is
    //    suit = S(index div 13)   where S(0)=Clubs, S(1)=Diamonds, S(2)=Hearts, S(3)=Spades
    //    value = V(index mod 13)  where V(1)=Ace, V(2)=2, ..., V(10)=10, 
    //                                   V(11)=Jack, V(12)=Queen, V(0)=King
    //    (div and mod refer to the integer division and remainder operations)
    //    for example, 3 => Three of Clubs
    //                 14 => Ace of Diamonds
    ...
}

Using Spec Fields for Specifications

In addition to their use in abstraction functions, spec fields are also useful for writing specifications of the ADT's operations.  Here's a specification for a method on the Line class:

/**
 * @requires start not equal to end
 * @return angle in radians between this line segment and a horizontal ray starting at start 
 * and extending to the right.  The angle is measured in a counter-clockwise direction.
 */
public double getAngle ();

Specifications may refer to specification fields, but never to representation fields. Rep fields depend on a particular implementation, so we don't want to expose them in a specification, which can be implemented in many different ways.

When you're writing specifications for operations, you may find it useful to define derived spec fields.  A derived spec field is just a spec field that can be written in terms of other spec fields.  In other words, it's a shorthand.  We use the syntax @derivedfield name : type // description = definition to define a derived field.  Like spec fields, this syntax appears in the class overview:

/**
 * Line represents an immutable line segment in the plane.
 * @specfield start : Point // start point
 * @specfield end : Point   // end point
 * @derivedfield length : real   // length of segment = dist(start, end)
 */

/**
 * Line represents an immutable line segment in the plane.
 * @specfield start : Point // start point
 * // THIS IS WRONG: refers to rep fields length and angle
 * @derivedfield end : Point   // end point = 
 *            end.x = start.x + length * cos(angle)
 *            end.y = start.x + length * cos(angle)
 */

/**
 * @requires length > 0
 * @return angle in radians between this line segment and a horizontal ray starting at start 
 * and extending to the right.  The angle is measured in a counter-clockwise direction.
 */
public double getAngle ();

Simplifying specifications is in fact the only real purpose of derived spec fields.

The presence of a specification field does not imply anything about the interface or implementation of the class. Although spec fields often correspond to observer methods, that's not always true.  The interface might not provide any observers that query the spec field's state, so clients of the class might not have access to the information stored in the spec field. Likewise, the implementation might not actually have a concrete field of the spec field's type: that information may be computed from multiple concrete fields, or it might not be available at all. The point is that specification fields are a convenience for use in abstraction functions and specifications.

Rep Invariants

 // Rep invariant is
 //    RI(r) = r.name != null && r.balance >= 0

 // Rep invariant is
 //    name != null && balance >= 0

 //    for all i, transactions[i] instanceof Trans

 //    suit in {Clubs,Diamonds,Hearts,Spades}

 //    string contains no duplicate characters

 //    size = number of non-null entries in array 

(1)   //    balance == sum (for all i) of transactions[i].amount

(2)   //    balance == sum (for all i) of transactions[i].getAmount()

(3)   //    balance == sum (for all i) of transactions.get(i).getAmount()

Choosing the Rep Invariant

public class Card {
    private int index;

    // Abstraction function is
    //    suit = S(index div 13)   where S(0)=Clubs, S(1)=Diamonds, S(2)=Hearts, S(3)=Spades
    //    value = V(index mod 13)  where V(1)=Ace, V(2)=2, ..., V(10)=10, V(11)=Jack, V(12)=Queen,
    //                                   V(0)=King
    ...
}

    // Rep invariant is
    //    0 <= index <= 51

/** CharSet represents a mutable set of characters. */
public class CharSet {
    private StringBuffer chars;

    // Abstraction function is
    //    { chars[i] | 0 <= i < chars.size }
    ...

    /** @modifies this
     *  @effects this_post = this - {c}
     */
    public void remove (char c) {
        int i = chars.indexOf(Character.toString (c));
        if (i != -1) chars.deleteCharAt (i);
    }
}

    //   name != null && transactions != null

• divide by zero
• index out of range
• class cast exception
  

    //   for all i, transactions[i] instanceof Trans

    //   transactions is a list of Trans objects      (less mathematical, probably clearer)

    //   studentsToSections maps Student to Integer

    List<Trans> transactions; // this syntax works only in Java 1.5
    Map<Student,Integer> studentsToSections; // only in Java 1.5

    List/*<Trans>*/ transactions;
    Map/*<Student,Integer>*/ studentsToSections;

Checking the Rep Invariant at Runtime

/** @effects: nothing if this satisfies rep invariant;
              otherwise throws an exception
*/
private void checkRep () {
    if (balance < 0) 
        throw new RuntimeException ("balance should be >= 0");

    if (name == null)
        throw new RuntimeException ("name should be non-null");

    // for all j, sum (i=0..j) transactions[i].amount >= 0
    int b = 0;
    for (int i = 0; i < transactions.size(); i++) {
        Trans t = (Trans) transactions.get(i);
        b += t.getAmount();
        if (b < 0)
           throw new RuntimeException("balance went negative");   
    }
    // balance = sum (for all i) transactions[i].amount
    if (balance != b)
        throw new RuntimeException ("balance should equal sum of transactions[i].amount");
}

    // using junit.framework.Assert (you don't have to be writing a unit test to use this class)
    Assert.assertTrue ("balance should be >= 0", balance >= 0); 

    // using Java 1.4 assert syntax
    assert balance >= 0 : "balance should be >= 0"; 

A Complete Example

/**
 * Card represents an immutable playing card.
 * @specfield suit : {Clubs,Diamonds,Hearts,Spades} // card suit
 * @specfield value : {Ace,2,...,10,Jack,Queen,King} // card rank
 */
public class Card {

    private int index;

    // Abstraction function is
    //    suit = S(index div 13)   where S(0)=Clubs, S(1)=Diamonds, S(2)=Hearts, S(3)=Spades
    //    value = V(index mod 13)  where V(1)=Ace, V(2)=2, ..., V(10)=10, V(11)=Jack, V(12)=Queen,
    //                                   V(0)=King

    // Rep invariant is
    //    0 <= index <= 51

    /** 
     * Check the rep invariant.
     * @effects: nothing if this satisfies rep invariant;
     *           otherwise throws an exception
     */
    private void checkRep() {
        if (index < 0 || index > 51)
            throw new RuntimeException ("card index out of range");
    }

    /**
     * @effects makes a new playing card with given suit and value
     */
    public Card(CardSuit suit, CardValue value) {
        ... // initialize Card
        checkRep ();
    }

    /**
     * @effects returns this.suit   <=== "suit" refers to the spec field
     */
    public CardSuit getSuit() {
        checkRep ();

        CardSuit s = ... // decode suit

        checkRep ();
        return s;
    }

    /**
     * @effects returns this.value  <=== "value" is the spec field
     */
    public CardValue getValue() {
       checkRep ();

       CardValue v = ... // decode value

       checkRep ();
       return v;
    }

    ...
}

General Hints on Readability

    // Abstraction function is
    //    <[x,y],s^[for all 0<i<=chars.size(), chars[chars.size()-i]]> | x=front.cdr, 
    //     y=back.car, s=n.toString()>

• Introduce new names where they're useful:
  

      AF(r) = list l such that...
  
      AF(r) = c_0 + c_1*x + c_2*x^2 + ...
          where c_i = ...
  

• Use spec fields:
  

      suit = ...
      value = ...

• Provide examples:
  

      for example, 3 => Three of Clubs 
  

• Introduce new functions where they're useful:
  

      reverse(back)

• Use plain language wherever it's unambiguous and clearer or more concise than formal syntax:
  

      chars contains no duplicates
  

  Contrast this with the formal alternative:
  

      for all 0<=i<j<chars.size, chars[i] != chars[j]