6.102
6.102 — Software Construction
Spring 2025

Code Examples for Reading 7

Download

You can also download a ZIP file containing this code.

After downloading and unpacking the ZIP file:

  • npm install to install package dependencies;
  • npm run to see a list of the ways this code can be run.
    • For example, if npm run shows that there are scripts called foo and bar, you can run the code with either npm run foo or npm run bar.
    • Two conventional script names are test and start. If the code includes one of those script names, then you can omit run and just say npm test or npm start.
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.

charset.ts

import assert from 'node: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.

    // assert the rep invariant
    private checkRep(): void {
        for (let i = 0; i < this.s.length; ++i) {
            const c = this.s[i];
            assert(c !== undefined);
            assert(this.s.indexOf(c, 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.
    
    // assert the rep invariant
    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];
            assert(c !== undefined);
            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) {
            const thisChar = this.chars[i];
            assert(thisChar !== undefined);
            if (thisChar === c) {
                return { found: true, index: i };
            } else if (thisChar > 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()

}

ratnum.ts

import assert from 'node: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

    // assert the rep invariant
    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;    
}

timespan.ts

import assert from 'node: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);
        this._end = new Date(end);
        this.checkRep();
    }

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

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

    // TODO: toString()

}