Управление потоком: итоги и задачи повышенной трудности

Чего достиг раздел

Раздел ставил целью научить управлять порядком выполнения с помощью ветвлений и циклов и рассуждать об их правильности: чтобы каждый случай был обработан, чтобы каждый цикл делал то, что должен, и чтобы он завершался. Цель достигнута с опорой только на то, что введение объявило известным: условия раздела 3, типы раздела 2, а также трассировку и вариант цикла из урока 1.1. Программа, которая вычисляла наибольший общий делитель за три фиксированных шага и в зависимости от данных отвечала неверно или делила на нуль, уступила место циклу из трёх строк, и теперь можно доказать, что этот цикл правилен для всех неотрицательных данных.

Ветвления

Урок Ветвления научил оператору if, всегда с фигурными скобками. Он показал, что в цепочке else if выполняется первая ветвь, условие которой истинно, так что настоящий случай каждой ветви есть её условие вместе с отрицанием всех условий, стоящих выше; отсюда важность порядка и то, что ветвь может оказаться недостижимой без всякого предупреждения. Он установил критерий правильности любого ветвления: его случаи должны не пересекаться (это обеспечивает форма цепочки) и исчерпывать все возможности (это так, если цепочка заканчивается на else), а также совпадать со случаями спецификации, что тестируется внутри каждого случая и по обе стороны каждой границы. Он представил условный оператор, позволяющий выбрать одно из двух коротких значений без целого ветвления. Завершился он enum class и switch, о пропущенном случае которого предупреждает компилятор.

Циклы

Урок Циклы представил while, do и for как три формы одного механизма: while вычисляет своё условие перед каждой итерацией и может не выполнить ни одной; do выполняет хотя бы одну; for собирает в заголовке инициализацию, условие и приращение, а его переменная цикла живёт только внутри цикла. Он научил их равносильности, таблице трассировки, с $k + 1$ вычислениями условия на $k$ итераций цикла while, который завершается по своему условию (и $k$ вычислениями в do), и подсчёту итераций по заголовку, который предупреждает ошибку на единицу. Он добавил break, continue и вложенные циклы, внутреннее тело которых выполняется столько раз, сколько даёт сумма: $m \cdot p$ при фиксированных границах, $n(n + 1)/2$ в треугольном случае.

Проектирование правильных циклов

Урок Проектирование правильных циклов сделал цикл объектом проектирования. Он собрал шаблоны (счётчик, накопитель, максимум и минимум, сигнальное значение и флаг), каждый из которых определяется тем, что означает его переменная после каждой итерации. Он определил инвариант, утверждение, верное всякий раз, когда вычисляется условие, с тремя его обязательствами: инициализацией, сохранением и завершением, которое вместе с ложным условием даёт постусловие; и распознал в нём индукцию по числу итераций. Он научил проектировать в обратном направлении, от постусловия к инварианту и от инварианта к телу. Он обосновал завершение вариантом цикла и показал три цикла, в которых арифметика C++ делает его недействительным: вещественный, который перескакивает 1.0, беззнаковый счётчик, который совершает оборот, и знаковый счётчик, который переполняется. Наконец, он дал первое знакомство с отладчиком.

Численные алгоритмы

Урок Численные алгоритмы применил всё это к четырём классическим алгоритмам, написанным внутри main и доказанным. Тест на простоту перебором делителей, с утверждением, что достаточно дойти до $\sqrt{n}$, и с условием d <= n / d, которое не переполняется там, где d * d <= n переполняется. Алгоритм Евклида, с инвариантом $\operatorname{\text{НОД}}(a, b) = \operatorname{\text{НОД}}(a_0, b_0)$ и вариантом цикла $b$, и две его опасности в C++: отрицательный результат и деление на нуль, если условие вычисляется после тела. Перевод в другую систему счисления последовательными делениями и схему Горнера, которая вычисляет значение многочлена с одним умножением на коэффициент. И метод бисекции, гарантированный теоремой о промежуточном значении и управляемый целым счётчиком, число итераций которого вычисляется заранее.