Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Imperative programming (resit) / 2 / c

Before testing candidate $i$, every earlier integer has been printed exactly when it belongs to the spectrum, and every positive $h<k$ satisfies $r{h}^2<i^2$. During the inner loop that exclusion remains true: an excluded candidate is passed over only after checking its square.

At termination of the inner loop, $r{k}^2\ge i^2$, so $k$ is the least positive possible witness. If its square is already at least $(i+1{)}^2$, every larger witness is too large as well; otherwise it satisfies both required inequalities and $i$ is printed. Advancing $i$ preserves the earlier-witness exclusion because the new lower bound only increases. These loop invariants establish both completeness and absence of extra outputs.