Code Examples for Reading 11

You can also download a ZIP file containing this code.

Seems to be necessary to have a triple-backtick block at the start of this page,
otherwise all the pre/code tags below aren't syntax highlighted.
So create a hidden one.

package charset;

/**
 * A mutable set of characters.
 */
public class CharSet1 implements Set<Character> {

    private String s = "";

    // Rep invariant:
    //   s contains no repeated characters
    // Abstraction function:
    //   AF(s) = {s[i] | 0 <= i < s.length()}
    // Safety from rep exposure:
    //   All fields are private and immutable.

    // Check that the rep invariant is true
    // *** Warning: this does nothing unless you turn on assertion checking
    // by passing -enableassertions to Java
    private void checkRep() {
        for (int i = 0; i < s.length(); ++i) {
            assert s.indexOf(s.charAt(i), i+1) == -1; // c not found in rest of string
        }
    }
    
    /**
     * Make a new empty character set.
     */
    public CharSet1() {
        checkRep();
    }
    
    @Override
    public int size() {
        checkRep();
        return s.length();
    }

    @Override
    public boolean contains(Character e) {
        checkRep();
        return s.indexOf(e) != -1;
    }

    @Override
    public void add(Character e) {
        if (!contains(e)) s += e;
        checkRep();
    }

    @Override
    public void remove(Character e) {
        int i = s.indexOf(e);
        if (i != -1) s = s.substring(0, i) + s.substring(i+1, s.length());
        checkRep();
    }
    
    // TODO: toString()

}

package charset;

/**
 * A mutable set of characters.
 */
public class CharSet2 implements Set<Character> {

    private String s = "";
    
    // Rep invariant:
    //   true (i.e., s is a non-null String, but no more assumptions are made)
    // Abstraction function:
    //   AF(s) = {s[i] | 0 <= i < s.length()}
    // Safety from rep exposure:
    //   All fields are private and immutable.
    
    private void checkRep() {
        assert s != null;
    }
    
    /**
     * Make a new empty character set.
     */
    public CharSet2() {
        checkRep();
    }
    
    @Override
    public int size() {
        int n = 0;
        for (int i = 0; i < s.length(); ++i) {
            char c = s.charAt(i);
            if (s.indexOf(c, i+1) == -1) {
                // This is the last time c occurs in s, so
                // count it now.  This avoid double-counting
                // characters that occur more than once.
                ++n;
            }
        }
        checkRep();
        return n;
    }

    @Override
    public boolean contains(Character e) {
        checkRep();
        return s.indexOf(e) != -1;
    }

    @Override
    public void add(Character e) {
        s += e;
        checkRep();
    }

    @Override
    public void remove(Character e) {
        // find and delete ALL occurrences of e
        while (true) {
            int i = s.indexOf(e); 
            if (i == -1) break;
            s = s.substring(0, i) + s.substring(i+1, s.length());
        }
        checkRep();
    }
    
    // TODO: toString()

}

package charset;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;

/**
 * A mutable set of characters.
 */
public class CharSet3 implements Set<Character> {

    private List<Character> chars = new ArrayList<>();
    
    // Rep Invariant:
    //   chars is sorted in increasing order with no repeated characters, so
    //       chars.get(i) < chars.get(i+1) for all 0<=i<chars.size()-1
    // Abstraction function:
    //   AF(s) = {chars.get(i) | 0 <= i < s.length()}
    // Safety from rep exposure:
    //   All fields are private.  The rep contains only one mutable type,
    //   List<Character>, and none of the parameters or return values of the public
    //   methods have that type, so they can't expose any aliases to the rep.
    
    private void checkRep() {
        boolean first = true;
        char previousC = 0;
        for (Character c : chars) {
            if (!first) assert previousC < c;
            first = false;
            previousC = c;
        }
    }
    
    /**
     * Make a new empty character set.
     */
    public CharSet3() {
        checkRep();
    }
    
    @Override
    public int size() {
        checkRep();
        return chars.size();
    }

    @Override
    public boolean contains(Character e) {
        checkRep();
        return Collections.binarySearch(chars,  e) >= 0;
    }

    @Override
    public void add(Character e) {
        int i = Collections.binarySearch(chars,  e);
        if (i < 0) {
            // not yet in set
            chars.add(-i-1, e);
        }
        checkRep();
    }

    @Override
    public void remove(Character e) {
        // find and delete ALL occurrences of e
        for (int i = 0; i < chars.size(); ++i) {
            if (chars.get(i) == e) {
                chars.remove(i);
                break;
            }
        }
        checkRep();
    }
    
    // TODO: toString()

}

/**
 * RatNum is an immutable type representing rational numbers.
 */
public class RatNum {

    private final int numerator;
    private final int denominator;

    // Rep invariant:
    //   denominator > 0
    //   numerator/denominator is in reduced form, i.e. gcd(|numerator|,denominator) = 1
    // Abstraction function:
    //   AF(numerator, denominator) = numerator/denominator
    // Safety from rep exposure:
    //   All fields are private, and all types in the rep are immutable.

    /**
     * Make a new RatNum == n.
     * @param n value
     */
    public RatNum(int n) {
        numerator = n;
        denominator = 1;
        checkRep();
    }

    /**
     * Make a new RatNum == (n / d).
     * @param n numerator
     * @param d denominator
     * @throws ArithmeticException if d == 0
     */
    public RatNum(int n, int d) {
        // reduce ratio to lowest terms
        int g = gcd(n, d);
        n = n / g;
        d = d / g;

        // make denominator positive
        if (d < 0) {
            numerator = -n;
            denominator = -d;
        } else {
            numerator = n;
            denominator = d;
        }
        checkRep();
    }

    /////////////////////////////////////////
    // other methods should go here
    //    producers: add(), subtract(), multiply(), divide(), etc.
    //    observers: isPositive(), intValue(), etc.
    //    mutators: none

    // Check that the rep invariant is true
    // *** Warning: this does nothing unless you turn on assertion checking
    // by passing -enableassertions to Java
    private void checkRep() {
        assert denominator > 0;
        assert gcd(Math.abs(numerator), denominator) == 1;
    }
    
    /**
     * @return a string representation of this rational number
     */
    @Override
    public String toString() {
        checkRep();
        return (denominator > 1) ? (numerator + "/" + denominator) : (numerator + "");
    }

    // compute greatest common divisor of a and b
    private static int gcd(int a, int b) {
        return (b == 0) ? a : gcd(b, a % b);
    }    
    
    // TODO: this immutable type needs equals() and hashCode()
}

import java.util.Date;

/**
 * Immutable datatype representing an interval starting from one date/time and
 * ending at a later date/time. The interval includes its endpoints.
 */
public class Timespan {

    private final Date start;
    private final Date end;

    // Rep invariant:
    //   !end.before(start)
    // Abstraction function:
    //   AF(start, end) = the time interval from start to end, including the endpoints 
    // Safety from rep exposure:
    //   All fields are private and immutable. (<=== oops, incorrect! Date is a mutable type,
    //                                          so this safety argument needs to talk about how
    //                                          the Date objects are either not exposed or
    //                                          are defensively copied)

    private void checkRep() {
        assert !end.before(start);
    }
    
    /**
     * Make a Timespan.
     * 
     * @param start starting date/time
     * @param end ending date/time, requires end >= start
     */
    public Timespan(Date start, Date end) {
        if (start.after(end)) {
            throw new IllegalArgumentException("requires start <= end");
        }
        this.start = new Date(start.getTime());
        this.end = new Date(end.getTime());
        checkRep();
    }

    /**
     * @return the starting point of the interval
     */
    public Date getStart() {
        return new Date(start.getTime());
    }

    /**
     * @return the ending point of the interval
     */
    public Date getEnd() {
        return new Date(end.getTime());
    }
    
    // TODO: toString()
    
    // TODO: this immutable type needs equals() and hashCode()

}