SpecCraft

SpecCraft is about formal methods in TypeScript projects. Below are some situations we run into from time to time. See if any of them look familiar, and learn how formal methods (and other modern tools) can help.

Connect on first use

Connect to the database on first use, then reuse the connection. Two requests at startup both see no connection yet, and both connect.

Before the fix Diff With the fix

export function lazyConnect<T>(connect: () => Promise<T>) {
  let db: Promise<T> | undefined;
  return async () => {
    if (!db) db = await connect();
    if (!db) {
      db = connect().catch((e) => {
        db = undefined;
        throw e;
      });
    }
    return db;
  };
}

See how TLA+ finds it.

Search as you type

A search-as-you-type box sends a request on every keystroke and shows whatever comes back. Type “rea”, then “react”, and two requests are waiting for a reply. If the one for “rea” is slower, it arrives last and replaces the results: the box says “react”, the list shows results for “rea”.

Before the fix Diff With the fix

export function createSearch(fetchResults: (query: string) => Promise<string[]>) {
  const state = { query: '', results: [] as string[] };
  let latest = 0;
  async function onInput(query: string): Promise<void> {
    const id = ++latest;
    state.query = query;
    const results = await fetchResults(query);
    if (id === latest) state.results = results;
  }
  return { state, onInput };
}

See how Quint finds it.

Binary search over sorted ids

Finding an id in a sorted list. Tests for a found id and a missing id both pass, but indexOfId([10, 20, 30], 10) returns -1: when the search narrows down to one last element, the loop stops before looking at it.

Before the fix Diff With the fix

export function indexOfId(ids: readonly number[], target: number): number {
  let lo = 0;
  let hi = ids.length - 1;
  while (lo <= hi) {
    const mid = Math.floor((lo + hi) / 2);
    if (ids[mid] < target) lo = mid + 1;
    else if (ids[mid] > target) hi = mid - 1;
    else return mid;
  }
  return -1;
}

See how Dafny finds it.

A percentage discount

A price with a percentage discount and a cap. Nothing stops percent from being over 100, and the discount is then bigger than the price, unless the cap happens to catch it.

Before the fix Diff With the fix

function clampPercent(percent: number): number {
  return Math.max(0, Math.min(percent, 100));
}
export function applyDiscount(priceCents: number, percent: number, capCents: number): number {
  const discount = Math.min(Math.floor((priceCents * clampPercent(percent)) / 100), capCents);
  return priceCents - discount;
}

See how Lean finds it.