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.

import assert from 'assert';

/**
 * A mutable set of characters.
 */
export class CharSet1 {

    private s: string = "";

    // 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
    private checkRep():void {
        for (let i = 0; i < this.s.length; ++i) {
            assert(this.s.indexOf(this.s[i], i+1) === -1); // c not found in rest of string
        }
    }
    
    /**
     * Make a new empty character set.
     */
    public constructor() {
        this.checkRep();
    }
    
    /**
     * Get size of the set.
     * @returns the number of elements in this set
     */
    public size(): number {
        this.checkRep();
        return this.s.length;
    }

    /**
     * Test for membership.
     * @param c a character, must be length-1 string
     * @returns true iff this set contains c
     */
    public contains(c: string): boolean {
        this.checkRep();
        return this.s.indexOf(c) !== -1;
    }

    /**
     * Modifies this set by adding c to the set.
     * @param c character to add, must be length-1 string
     */    
    public add(c: string): void {
        if (!this.contains(c)) this.s += c;
        this.checkRep();
    }

    /**
     * Modifies this set by removing c, if found.
     * If c is not found in the set, has no effect.  
     * @param c character to add, must be length-1 string
     */
    public remove(c: string): void {
        const i = this.s.indexOf(c);
        if (i !== -1) this.s = this.s.substring(0, i) + this.s.substring(i+1, this.s.length);
        this.checkRep();
    }
    
    // TODO: toString()

}


/**
 * A mutable set of characters.
 */
export class CharSet2 {

    private s: String = "";
    
    // 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.
    
    // Check that the rep invariant is true
    private checkRep():void {
        // always true -- non-nullity guaranteed by static checking
    }

    /**
     * Make a new empty character set.
     */
    public constructor() {
        this.checkRep();
    }

    /**
     * Get size of the set.
     * @returns the number of elements in this set
     */    
    public size(): number {
        let n = 0;
        for (let i = 0; i < this.s.length; ++i) {
            const c = this.s[i]
            if (this.s.indexOf(c, i+1) === -1) {
                // This is the last time c occurs in s, so
                // count it now.  This avoids double-counting
                // characters that occur more than once.
                ++n;
            }
        }
        this.checkRep();
        return n;
    }

    /**
     * Test for membership.
     * @param c a character, must be length-1 string
     * @returns true iff this set contains c
     */
    public contains(c: string): boolean {
        this.checkRep();
        return this.s.indexOf(c) !== -1;
    }

    /**
     * Modifies this set by adding c to the set.
     * @param c character to add, must be length-1 string
     */
    public add(c: string): void {
        this.s += c;
        this.checkRep();
    }

    /**
     * Modifies this set by removing c, if found.
     * If c is not found in the set, has no effect.  
     * @param c character to add, must be length-1 string
     */
    public remove(c: string): void {
        // find and delete ALL occurrences of e
        while (true) {
            const i = this.s.indexOf(c);
            if (i === -1) break;
            this.s = this.s.substring(0, i) + this.s.substring(i+1, this.s.length);
        }
        this.checkRep();
    }
    
    // TODO: toString()

}


/**
 * A mutable set of characters.
 */
export class CharSet3 {

    private chars: Array<string> = [];
    
    // Rep Invariant:
    //   every string in chars has length-1
    //   chars is sorted in increasing order with no repeated characters, so
    //       chars[i] < chars[i+1] for all 0<=i<chars.length
    // Abstraction function:
    //   AF(s) = {chars[i] | 0 <= i < chars.length}
    // Safety from rep exposure:
    //   All fields are private.  The rep contains only one mutable type,
    //   Array<string>, 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 checkRep(): void {
        let previousC = ""; // guaranteed to be < any single-character string
        for (const c of this.chars) {
            assert(c.length === 1);
            assert(previousC < c);
            previousC = c;
        }
    }
    
    /**
     * Make a new empty character set.
     */
    public CharSet3() {
        this.checkRep();
    }

    /**
     * Get size of the set.
     * @returns the number of elements in this set
     */    
    public size(): number {
        this.checkRep();
        return this.chars.length;
    }

    /**
     * Find the location of a character in the sorted array this.chars,
     * or the location where it should be inserted if it's not present.
     * @param c character to search for; must be length-1
     * @returns found=true if and only if this.chars contains c;
     *          index is in the range [0, this.chars.length]
     *          where this.chars[index]=c if found,
     *                otherwise this.chars[index-1] < c  (if index > 0)
     *                          and c < (this.chars[index] (if index < this.chars.length)
     */
    private find(c: string): { found: boolean, index: number } {
        let i = 0;
        for (; i < this.chars.length; ++i) {
            if (this.chars[i] === c) {
                return { found: true, index: i };
            } else if (this.chars[i] > c) {
                return { found: false, index: i };
            }
        }
        return { found: false, index: this.chars.length };
    }

    /**
     * Test for membership.
     * @param c a character, must be length-1 string
     * @returns true iff this set contains c
     */
    public contains(c: string): boolean {
        this.checkRep();
        return this.find(c).found;
    }

    /**
     * Modifies this set by adding c to the set.
     * @param c character to add, must be length-1 string
     */
    public add(c: string): void {
        const {found, index} = this.find(c);
        if ( ! found ) {
            // not yet in set; insert it
            this.chars.splice(index, 0, c);
        }
        this.checkRep();
    }

    /**
     * Modifies this set by removing c, if found.
     * If c is not found in the set, has no effect.  
     * @param c character to add, must be length-1 string
     */
    public remove(c: string): void {
        const {found, index} = this.find(c);
        if (found) {
            this.chars.splice(index, 1);
        }
        this.checkRep();
    }
    
    // TODO: toString()

}

import assert from 'assert';

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

    private readonly numerator: bigint;
    private readonly denominator: bigint;

    // 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 / d).
     * @param n numerator
     * @param d denominator
     * @throws Error if d = 0
     */
    public constructor(n: bigint, d: bigint) {
        // reduce ratio to lowest terms
        const g = gcd(BigInt(n), BigInt(d));
        const reducedNumerator = n / g;
        const reducedDenominator = d / g;

        // make denominator positive
        if (d < 0n) {
            this.numerator = -reducedNumerator;
            this.denominator = -reducedDenominator;
        } else if (d > 0n) {
            this.numerator = reducedNumerator;
            this.denominator = reducedDenominator;
        } else {
            throw new Error('denominator is zero');
        }
        this.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
    private checkRep(): void {
        assert(this.denominator > 0n);
        assert(gcd(abs(this.numerator), this.denominator) === 1n);
    }
    
    /**
     * @returns a string representation of this rational number
     */
    public toString(): string {
        this.checkRep();
        return (this.denominator > 1n) ? (this.numerator + "/" + this.denominator) : (this.numerator + "");
    }

}

// compute greatest common divisor of a and b
function gcd(a: bigint, b: bigint): bigint {
    return (b === 0n) ? a : gcd(b, a % b);
}

// compute the absolute value of a bigint
function abs(x: bigint): bigint {
    return x < 0n ? -x : x;    
}

import assert from 'assert';

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

    private readonly _start: Date;
    private readonly _end: Date;

    // Rep invariant:
    //   start <= end
    // 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 checkRep(): void {
        assert(this.start <= this.end);
    }
    
    /**
     * Make a Timespan.
     * 
     * @param start starting date/time
     * @param end ending date/time, requires start <= end
     */
    public constructor(start: Date, end: Date) {
        if (start > end) {
            throw new Error("requires start <= end");
        }
        this._start = new Date(start.valueOf());
        this._end = new Date(end.valueOf());
        this.checkRep();
    }

    public get start() {
        return new Date(this._start.valueOf());
    }

    public get end() {
        return new Date(this._end.valueOf());
    }

    // TODO: toString()

}