Synthesis and challenges: control flow

What the unit achieved

The unit set out to teach how to govern the order of execution with decisions and loops, and how to reason about their correctness: that every case is handled, that every loop does what it must and that it terminates. The purpose has been fulfilled relying only on what the introduction declared it took for granted: the conditions of unit 3, the types of unit 2, and the trace and the variant of lesson 1.1. The program that computed the greatest common divisor with three fixed steps, and that, depending on the data, answered wrongly or divided by zero, was replaced by a three-line loop, and it can now be proved that this loop is correct for all nonnegative data.

Decisions

The lesson Decisions taught the if statement, always with braces. It showed that in a chain of else if the first branch whose condition is true is executed, so that the real case of each branch is its condition together with the negation of all the previous ones; hence order matters, and a branch can become unreachable without a warning. It established the correctness criterion of every decision: its cases must be disjoint (they are, by the form of the chain) and exhaustive (they are if it ends in else), and they must coincide with those of the specification, which is tested inside each case and on each side of each boundary. It introduced the conditional operator, to choose between two short values without a whole decision. It closed with enum class and switch, whose forgotten case the compiler warns about.

Loops

The lesson Loops presented while, do and for as three forms of a single mechanism: the while evaluates its condition before each iteration and may perform none; the do performs at least one; the for gathers in its header the initialization, the condition and the update, and its loop variable lives only in the loop. It taught their equivalences, the trace table, with $k + 1$ evaluations of the condition for $k$ iterations of a while that ends by its condition (and $k$ evaluations in a do), and counting the iterations from the header, which prevents the off-by-one error. It added break, continue and nested loops, whose inner body is executed a sum of times: $m \cdot p$ with fixed bounds, $n(n + 1)/2$ with the triangle.

Designing correct loops

The lesson Designing correct loops made the loop an object of design. It gathered the patterns (counter, accumulator, maximum and minimum, sentinel and flag), each defined by what its variable means after every iteration. It defined the invariant, a statement that holds every time the condition is evaluated, with its three obligations: initialization, maintenance and conclusion, which together with the false condition yields the postcondition; and it recognized it as an induction on the number of iterations. It taught how to design backwards, from the postcondition to the invariant and from the invariant to the body. It justified termination with the variant, and showed three loops in which the arithmetic of C++ invalidates it: the real-valued one that skips 1.0, the unsigned counter that wraps around and the signed counter that overflows. Finally, it gave a first contact with the debugger.

Numerical algorithms

The lesson Numerical algorithms applied all of the above to four classical algorithms, written inside main and proved. Primality by trial division, with the proposition that it suffices to reach $\sqrt{n}$ and with the condition d <= n / d, which does not overflow where d * d <= n does. The Euclidean algorithm, with the invariant $\operatorname{gcd}(a, b) = \operatorname{gcd}(a_0, b_0)$ and the variant $b$, and its two dangers in C++: the negative result and division by zero if the condition is evaluated after the body. Change of base by successive divisions and Horner’s rule, which evaluates a polynomial with one multiplication per coefficient. And bisection, guaranteed by the intermediate value theorem and governed by an integer counter whose number of iterations is computed in advance.