What does a single counterexample settle about the written claim that every schedule this scheduler produces is fair?
answer
- every-claim, single witness
- exhibit it, do not hypothesise it
- one run kills the sentence as written
- absence after searching proves nothing
- narrowing makes it a new claim
basics
~10 sOne exhibited run in which a ready task is passed over forever settles the claim as written: it is false, and no more evidence is needed. It says nothing about how often that happens.
solid answer
~50 sA claim about **every** schedule is refuted by **one** schedule. The counterexample has to be exhibited, not hypothesised: concrete inputs, a reachable state, and the point at which the claim's own words stop holding. Once it is on the table the claim is dead as written, and no argument for it can be correct — if someone still has a proof, the proof has a flaw and the counterexample tells you roughly where. What it does not give you is a measure: a run that needs an adversarial arrival pattern refutes the claim exactly as hard as one that happens hourly. It also does not repair anything. The usual response is to narrow the claim — add the hypothesis the counterexample violated — and then argue the narrowed claim, which is a new statement needing a new argument.
code
pseudocode · 8 linespick_next(queues): # fixed order, highest class first
for each q in queues:
if not empty(q):
return pop(q)
return none
# witness: arrivals keep queues[0] non-empty forever
# => a task sitting in queues[1] is never returnedgo deeper
Recall that a claim about every case is refuted by one concrete case, and that the case must be shown rather than described as something that could happen.
Be able to construct the witness: pick inputs, trace the run, and point at the moment the claim's own wording fails, then say what the refutation does and does not establish.
Show the review discipline: check the witness uses reachable state, resist the urge to rank it by likelihood before accepting it, and insist a narrowed claim gets a fresh argument.
Decide which claims in a design are worth a witness hunt at all, and set the expectation that a refuted claim is rewritten in the document rather than quietly softened into folklore.
## Why one witness is enough A claim of the form *every schedule this scheduler produces is fair* asserts something about an unbounded collection of runs. To establish it you must cover all of them; to demolish it you need exactly one. That asymmetry is the whole of disproof by counterexample, and it is why a reviewer's cheapest move against a suspicious claim is to hunt for a single run rather than to look for a flaw in someone's argument. The refutation is **total**, not statistical. There is no residue of the claim left standing, no *mostly true*, no *true in practice*. Either the document's sentence covers the exhibited run or it does not; if it does, it is false. ## What makes a counterexample admissible 1. **It is exhibited, not imagined.** *There could be a run where the first queue never drains* is a conjecture. *Here are the arrivals, here is the resulting order, here is the task never selected* is a counterexample. 2. **The state it uses is reachable.** A run assembled by writing values directly into internal structures refutes nothing about the scheduler; it refutes a claim about structures nobody promised. 3. **It is judged in the claim's own words.** If the document says *fair* and means *every ready task is eventually selected*, the run must violate that, not some stronger notion the reader supplied. 4. **It is checkable by someone else.** A counterexample is an artefact of review, so a second engineer must be able to replay it and agree. A scheduler that scans a fixed priority order and returns the first non-empty queue meets its claim only while high-priority work is intermittent. Exhibit a stream in which the first queue is never empty, and a task in the second queue is never selected at all. That is the whole refutation, and it took no theory. ## What one counterexample does not tell you - **Not frequency.** A witness that needs an adversarial arrival pattern refutes the sentence just as completely as one that reproduces on every deploy. Prioritisation is an engineering decision made after the logical one. - **Not the fix.** It marks a false sentence; it does not say whether the scheduler, the claim, or the requirement is the thing to change. - **Not the size of the failure.** One starved task and a systematically starved class of tasks may both come from the same witness. - **Not that the underlying idea is wrong.** Usually the claim was stated too broadly and holds under a hypothesis the writer forgot to state. ## When no counterexample turns up | | A counterexample is found | None found after a search | |---|---|---| | Status of the claim | false as written, settled | open — neither established nor refuted | | What you learned | the exact boundary the claim crosses | that the failure, if any, is not small or not in the shape searched | | Next move | narrow the claim, or change the code | attempt the argument, using the search's shape to guide it | A long unsuccessful hunt is **evidence, not proof**. Checking a claim on the first forty cases and finding nothing establishes only that no counterexample lives below forty. The stock illustration is the claim that `n^2 + n + 41` is prime for every non-negative integer `n`: it holds for `n` from 0 through 39, and fails at `n = 40`, where `1600 + 40 + 41 = 1681 = 41^2`. Forty consecutive confirmations bought nothing. On code the same trap appears as a claim confirmed by every test in the suite, because the suite and the claim were written by the same person with the same blind spot. ## Repairing the claim rather than the argument When a counterexample lands, the productive response is to work on the sentence: - **Strengthen the hypothesis.** *Every schedule is fair* becomes *every schedule in which each queue is empty infinitely often is fair* — that is precisely the condition the witness violated. - **Weaken the conclusion.** *Fair* becomes *no task in the highest non-empty class waits indefinitely*, if that is all the design actually needs. - **Change the mechanism** — add ageing so waiting raises a task's effective priority — and note that this is now a different scheduler, so the old witness must be replayed against it rather than assumed dead. Whichever you pick, the narrowed sentence is a **new claim**. It inherits no credibility from the old one, and it needs its own argument before it goes back into the document. The most common review failure at this point is to edit the claim until the known witness no longer applies and treat the edit as the proof.
- A team checked a claimed identity on the first forty inputs and found no counterexample — what has that established?Only that no counterexample exists in the range checked. The claim that `n^2 + n + 41` is prime survives every `n` from 0 to 39 and dies at `n = 40`, where the value is 1681, or 41 squared. On code, a suite that passes proves the same limited thing, and proves less when the suite and the claim share an author's blind spot.
- What do you do with a design claim once a counterexample lands?Fix the sentence, not the argument. Either strengthen the hypothesis so it excludes the witnessed situation, weaken the conclusion to what the design actually needs, or change the mechanism. Whichever you choose, the result is a new claim with no inherited credibility, and it needs its own argument and its own counterexample hunt.
saying these in an interview costs you the question
- Says a counterexample only shows the claim is usually true.
- Offers a hypothetical run instead of concrete inputs and a trace.
- Treats a long unsuccessful search as a proof of the claim.
- Dismisses a witness because the arrival pattern looks unlikely.
- Edits the claim until the witness misses and calls it proved.
- Builds the witness from an unreachable internal state.