skip to content

A retry loop re-fetches an index until the fetch succeeds, with no attempt cap — can you argue it terminates?

level: seniorimportance: should knowfreq 44%

answer

  1. the exit depends on the world, not the state
  2. no measure falls, so no variant
  3. if it exits versus it exits
  4. a cap turns the bound into a count
  5. the postcondition becomes a disjunction

basics

~20 s

No. Nothing in the loop's own state decreases, so there is no measure to exhibit; whether it stops depends on the world outside the code. You can still show partial correctness — if it exits, the fetch succeeded — and you get termination only by introducing a bound.

solid answer

~50 s

The loop is **unbounded**: its exit is a condition about an external event, and no quantity computed from the loop's state falls on each pass. So there is no variant, and termination is not a property of this code at all — it is a bet on the world. What you can still establish is **partial correctness**: *if* the loop exits, the fetch succeeded. To get total correctness you have to make the bound explicit, and an attempt counter is the honest choice because the attempts remaining is a genuine measure: a non-negative integer falling by one each pass. A deadline is a weaker argument, resting on the clock advancing by some minimum step. Either way the postcondition weakens to a disjunction — succeeded, or budget exhausted — and every caller must now handle the second branch.

code

pseudocode · 8 lines
pseudocode
attempts = 0
result = failure
while result is failure and attempts < max_attempts:
    result = fetch_index()
    attempts = attempts + 1
    if result is failure:
        wait(backoff(attempts))
// on exit: result is ok, OR attempts = max_attempts

go deeper

for a junior

Notice the shape: a loop that stops only when something outside it cooperates has no reason of its own to stop. Asking what happens if it never cooperates is the right instinct.

for a middle

Explain the split between what you can prove and what you cannot: if it exits, the fetch succeeded, but that it exits does not follow from the code. Then name the bound that would fix it.

for a senior

Show the operational consequence: which loops in a service can wedge, what the cap changes about the returned value, and why the exhausted branch needs a caller that handles it rather than a default that reads as success.

for a principal

Own the standard: where budgets are set, who is allowed to retry, and how an exhausted budget is reported upward so that capping one loop does not simply relocate the stall to the caller.

## Bounded and unbounded loops A **bounded** loop carries its own reason for stopping: something in the state it controls runs out — positions in a list, items on a work list, attempts remaining. An **unbounded** loop stops only when the world outside it cooperates: a fetch succeeds, a lock is released, a message arrives. The distinction is not about the syntax used to write the loop; it is about whether the exit condition is a function of state the loop changes. The retry described here is unbounded. The body calls out, gets a failure, waits, and calls out again. Nothing it computes gets smaller. Ask for a measure and there is none to give — and that is the right answer, not a gap in the candidate's imagination. ## Partial correctness versus total correctness This is where the two readings of a correctness claim come apart. A **Hoare triple** — precondition, code, postcondition — has a partial reading and a total one: - **Partial:** if the code terminates, the postcondition holds. This the retry loop satisfies easily: the only way out is the success test, so on exit the fetch succeeded. - **Total:** the code terminates **and** the postcondition holds. This it cannot satisfy, because the first conjunct is unprovable from the code. Saying "it terminates because the fetch will eventually succeed" is not a proof; it is an assumption about the environment, and it is exactly the assumption that fails on the day the remote index is gone for good rather than briefly unavailable. ## Making the bound explicit The repair is to move the bound from the environment into the loop: 1. **Choose a budget** the caller can live with: a number of attempts, a deadline, or both. 2. **Make it the measure.** Attempts remaining is a non-negative integer that falls by one per pass — a variant, and the loop is now bounded. 3. **Weaken the postcondition to a disjunction:** on exit, either the fetch succeeded, or the budget ran out. 4. **Force the caller to handle both.** Return a value that distinguishes them, so the exhausted case cannot be mistaken for success by a caller reading an uninitialised result. Step 4 is the one teams skip, and it is why a capped retry sometimes turns a hang into a silent wrong answer, which is worse. ## The two bounds are not the same argument | Bound | Measure | Strength of the argument | |---|---|---| | None — retry until success | none exists | partial correctness only; may run forever | | Attempt cap | attempts remaining, a falling non-negative integer | a genuine variant; the loop always stops | | Deadline | time left, in a dense range | holds only if the clock advances by a minimum step each pass | | Cap plus deadline | whichever runs out first | stops on the earlier of the two | A deadline reads as obviously sufficient and is subtly weaker: a measure over a dense quantity can shrink forever without running out, which is the same trap that makes a halving backoff useless as a variant. In practice a clock does advance in steps, and each pass includes a wait, so the argument goes through — but say the step out loud rather than leaving it implicit. That is the difference between an engineer who has reasoned about it and one who is reciting a pattern. ## Not every unbounded loop is a defect Some loops are meant never to terminate: a loop that waits for work, handles it, and waits again is doing its job precisely by not stopping. For those, the obligation changes rather than disappears: - **Each pass** terminates, so the loop cannot wedge inside one iteration. - Nothing pending is lost when a pass ends. - There is a way to make it stop from outside, and that way is a condition the loop actually tests. The defect is not unboundedness itself; it is an unbounded loop whose *caller* believes it is bounded. ## What the interviewer is testing Not whether you know a retry needs a cap — everyone says that. It is whether you can say **what** you can and cannot prove about the uncapped version, and what the cap actually changes: not just the running time, but the postcondition, and therefore the contract every caller is written against.

  • Is an unbounded loop always a defect?
    No. A loop that waits for work, handles it and waits again is meant not to stop. What it still owes is that each pass terminates, that nothing pending is dropped when a pass ends, and that there is an outside condition it actually tests so it can be told to stop. The defect is an unbounded loop whose caller believes it is bounded.
  • Once you add an attempt cap, what must change outside the loop?
    The contract. The postcondition is now a disjunction — the fetch succeeded, or the budget ran out — so the value handed back must distinguish the two and every caller must have a branch for the exhausted case. Skipping that converts a visible hang into a silent wrong answer.

saying these in an interview costs you the question

  • Claims it terminates because the fetch will eventually succeed
  • Treats a shrinking backoff delay as the measure that falls
  • Says an unbounded loop is always a bug in any context
  • Adds a cap and leaves the postcondition and callers unchanged
  • Offers 'it has never hung in testing' as a termination argument