Skip to main content

Translating Informal Problems into Formal Specifications

What This Concept Is​

A formal specification is a precise description of what a solver must produce, written tightly enough to decide whether an implementation satisfies it. A relational specification may intentionally accept several outputs. It has a fixed shape:

  • inputs: types, ranges, pre-conditions
  • outputs: types, post-conditions
  • invariants: things that must stay true across the computation or across the system state
  • constraints: time, memory, throughput, correctness tolerances
  • failure modes: what happens on bad input, missing data, overflow, ties, duplicates
  • determinism policy: is the answer unique, or are multiple answers acceptable?

An informal problem is what you are actually handed: a sentence from a product manager, a chat message from a teammate, a contest prompt in English, a screenshot. Informal problems are almost always under-specified, sometimes over-specified, and often internally inconsistent.

Translation is the disciplined work of turning the informal artifact into the formal one. It is problem-solving in its own right -- a direct extension of Polya's understanding phase into the code world.

The distinction worth fixing early: a specification answers "what would be correct?", a plan answers "how will we produce something correct?", and an implementation answers "what did we actually produce?". Many projects confuse these. A missing or bad spec makes the plan and implementation ungrounded; all disputes become opinion.

Why It Matters Here​

Module 5 earlier treats "understand the problem" as a mathematical habit (see concept 1). Once you leave textbooks, the understanding phase no longer happens against a carefully-written problem statement. It happens against ambiguity.

Without a spec:

  • you build the wrong thing, correctly
  • tests pass but reviewers reject the behaviour
  • the next person cannot tell whether an edge case is a bug or a feature
  • you cannot verify your own work, because there is nothing to verify against

The spec is the artifact everything else verifies against. Proofs verify against a theorem statement; code verifies against a spec. Skipping the spec is skipping the only ground truth you have.

Forward pipeline: Semester 2 (algorithm-design chapters open with formal I/O statements), Semester 3 (refactoring preserves a specified contract, not just observed behaviour), Semester 4 (systems programming forces API contracts to be machine-checkable), Semester 5 (distributed-systems protocols are formal specs), Semester 7 (ADR context + decision is a lightweight formal spec at architecture scale), Semester 10 (the capstone hinges on a stable problem statement through scope changes).

Concrete Examples​

Example 1 -- separate filtering from ranking​

Specify a pure ranking function whose input is already filtered to a declared window. For a combined filter-and-rank function, pass now explicitly and use the half-open UTC interval [now - 24 hours, now). Its output is a permutation of the selected records, not necessarily of the full input. State whether future timestamps are rejected or excluded. Fix one example with records exactly at both endpoints; it distinguishes policies that otherwise look identical.

Use an agreed score and deterministic tie rule such as descending score, then ascending unique ID. Reject non-finite scores, duplicate IDs, or explicitly define their treatment. Ranking is not proof of fraud. Any latency target also needs a workload, machine, measurement boundary, and repeat protocol.

Example 2 -- deduplication is an identity decision​

Two records sharing an ID can be corrupt or refer to a reused identifier. Email normalisation can merge distinct mailboxes. Preserve email local-part case and do not strip provider-specific tags by default; SMTP treats local parts as case-sensitive, while domains are case-insensitive. See RFC 5321 section 2.3.11. Provider-specific equivalence requires an explicit, justified policy.

For this module, deduplicate exact opaque IDs, keep the earliest input record, and report conflicts instead of merging fields silently. State that this is record-key equality, not verified human identity. Fuzzy matching may be deterministic with fixed rules but still wrong about identity. Avoid asserting a universal runtime for it; candidate generation and comparison costs matter.

Common Confusion / Misconceptions​

Over-specification. Writing a spec so tight that it constrains the implementation instead of the behaviour. "Use a min-heap" is an implementation choice, not a spec. The spec says what, not how.

Under-specification. Leaving tie-breaking, null handling, or determinism unstated. Every under-specified corner is a future bug argument. Resolve it in the spec or explicitly mark it as "caller's choice."

Accidental non-determinism. Silently accepting Python's dictionary iteration order, floating-point summation order, or wall-clock-dependent inputs without flagging them. Non-determinism is a spec choice; it must be declared, not inherited.

Spec drift. The code evolves; the spec does not. After two features, the spec no longer describes the code. Either the spec is a living document or it is worthless.

Specs for proofs vs. specs for code. A proof spec (theorem statement) must be true; it does not care how you got there. A code spec must additionally be checkable at runtime (types), testable (you can write cases for each post-condition), and performant (constraints declare the cost envelope).

How To Use It​

Translation protocol:

  1. Read the informal prompt once, without thinking about solutions.
  2. List every noun. For each, ask: is this a type I can name? What are its fields, ranges, null behaviour?
  3. List every verb. For each, ask: what is the pre-condition, what is the post-condition, what is left unchanged?
  4. Name three concrete tiny examples you expect to work. Write input -> output.
  5. Name three adversarial tiny examples: ties, empty input, single element, duplicate values, out-of-range, nulls.
  6. For every adversarial case, write the intended output. If you cannot, the spec is missing a rule. Add the rule.
  7. State one performance constraint and one determinism constraint explicitly.
  8. Re-read the spec. If a reviewer could implement a behaviorally different but "spec-conforming" solution, tighten it.

This is concept 1's understanding phase executed with an engineering vocabulary.

Transfer / Where This Shows Up Later​

  • Semester 2 (algorithms). Every algorithm is introduced with a formal I/O contract. Without it, correctness claims are meaningless.
  • Semester 3 (refactoring & design patterns). Refactoring preserves a spec; design patterns are specs for recurring structural problems.
  • Semester 4 (systems programming). API contracts (POSIX, system calls) are specifications with machine-checkable pre- and post-conditions.
  • Semester 5 (networks & distributed systems). Protocols -- TCP, HTTP, gRPC -- are prose specifications governing millions of implementations.
  • Semester 7 (architecture). ADRs pair a context (the spec's pre-conditions) with a decision (the behavioural commitment). Fitness functions turn the spec's non-functional clauses into automated checks.
  • Semester 10 (capstone). A stable problem statement is the capstone's single most important artifact; stakeholders mutate prompts weekly, and the spec is your only defence against scope drift.

Check Yourself​

  1. Why is "sort the transactions" under-specified, and what is the minimum additional information required to make it specified?
  2. What is the difference between over-specification and under-specification, and why are both harmful?
  3. Why is a spec for code typically more detailed than a spec for a proof? Give two concrete things a code spec must declare that a proof spec may leave implicit.
  4. Give an example of an "accidental non-determinism" bug and describe how the spec should prevent it.
  5. What counts as evidence that a spec is complete? (Hint: think about peer verification.)

Mini Drill or Application​

Drill A. Take one of these informal prompts and write a full spec following the eight-step protocol above:

  1. "Show the user their most important notifications at the top."
  2. "Find the shortest delivery route for a fleet of trucks today."
  3. "Produce a daily report of active users."

The spec you write will be longer than the prompt. That is the point. When you have finished, swap with a peer: can they implement it without asking you a single question? If yes, the spec holds.

Drill B. Re-read the fraud-sorting spec in Example 1 and add a new constraint: "the fraud team wants to be able to filter to only the top 100 suspicious transactions". Update the spec. What changes in the I/O? What new failure modes emerge?

Drill C (unseen). You are handed: "detect bot traffic on the signup page." List at least six ambiguities the prompt contains, and for each state the minimal resolution you would propose. Draft the I/O section of the spec with types.

Read This Only If Stuck​

Engineering extension: Budget exhaustion is not impossibility​

A search API should distinguish found(witness), unreachable after complete exploration of a specified finite domain, and unknown after a time or state budget. Invalid input is separate. Test all statuses. An empty path can mean start equals goal; it must not double as a failure sentinel. Supply the model version and search bound with any negative claim.

Continue with the evidence contracts and the practice feedback after an independent attempt.