Chapter 5：Loops and Relational Expressions

为什么循环需要证明而不只是重复

循环把一段代码执行多次，也把一个小错误放大多次。正确循环必须说明：第一次测试前状态合法；每轮开始时哪些事实保持；循环体怎样推进；何时退出；退出后结果满足什么。只写“重复 count 次”无法证明数组访问、输入失败和动态边界。

关系表达式定义继续执行的集合

< <= > >= == != 比较操作数并产生 bool。条件 i < count 表示 i 仍位于半开区间；i <= count 则额外包含尾后位置。先把合法集合写成区间，再选择运算符，比靠记忆“通常用小于号”更可靠。

signed 与 unsigned 混合比较可能先转换负数，浮点相等比较受近似影响。关系表达式的语法简单，但操作数类型和领域含义仍来自 Chapter 3 的转换契约。

for 循环把计数生命周期放在头部

for 循环适合初始化、继续条件和更新都围绕一个局部计数器的场景。下面的不变量是：进入第 i 轮时，total 等于 values[0..i) 的和；更新后 i 增一，未处理元素严格减少。

int values[4]{3, 5, 7, 9};
int total{0};
for (int i{0}; i < 4; ++i) {
    total += values[i];
}

若循环体修改 i、count 或容器长度，不变量需要重新证明。计数器作用域限制在 for 内可减少误用；若循环后仍需最终 i，应显式说明原因而不是扩大作用域图方便。

while 循环让外部状态驱动重复

while 循环先测试条件，可能一次也不执行，适合“只要输入成功就继续”或“只要工作队列非空就处理”。把产生新值的读取操作放进条件，能避免 EOF 后沿用旧字符。

char ch{};
int letters{0};
while (std::cin.get(ch) && ch != '#') {
    if (ch >= 'A' && ch <= 'Z') {
        ++letters;
    }
}

这里有两个退出原因：流无法再产生字符，或读到业务哨兵 #。退出后若要报告原因，应分别检查；不要把 EOF 当成普通字符，也不要写 while (!cin.eof()) 后再读取。

do while 表达至少一次执行

do while 先执行循环体再检查，适合先显示菜单/读取一次，然后决定是否重复。它不适合第一次执行也需要前置条件的操作；“至少一次”必须来自业务契约，而不是为了少写一段代码。

int choice{0};
do {
    std::cout << "1: run, 0: quit\n";
    if (!(std::cin >> choice)) {
        break;
    }
} while (choice != 0);

break 在输入失败时离开循环，但多个 break 会增加退出路径。每条退出都要有后置状态；若循环后必须区分用户退出与格式错误，保存原因而不是只看 choice。

范围 for 用元素遍历替代手工下标

C++11 范围 for 适合访问范围中的每个元素。for (int value : values) 复制元素，修改 value 不影响数组；for (int& value : values) 绑定可写引用；只读且避免复制可用 const auto&。

for (int& value : values) {
    value *= 2;
}

范围 for 减少 off-by-one，但不能自动保证在遍历时修改容器结构安全。使 vector 重分配或使迭代器失效的操作仍需查容器契约。

文本输入循环必须把读取成功纳入条件

格式化 >> 默认跳过空白，get() 可以逐字符读取并保留空格和换行。选择取决于处理单位：读取数字/单词用格式化提取，统计原始字符用 get。两者都应由读取成功驱动循环。

若读取失败后只清除状态却不移除导致失败的字符，下一次读取会再次失败，形成不终止循环。恢复协议需要识别错误、清除状态、丢弃或重新解析输入，并设置尝试次数边界。

嵌套循环分别证明每个维度

二维数组 grid[rows][cols] 是 rows 个行数组，每行含 cols 个元素。外层行下标满足 [0,rows)，内层列下标满足 [0,cols)；总访问次数 rows*cols 不能替代逐维边界。

int grid[2][3]{{1, 2, 3}, {4, 5, 6}};
for (int row{0}; row < 2; ++row) {
    for (int col{0}; col < 3; ++col) {
        std::cout << grid[row][col] << ' ';
    }
    std::cout << '\n';
}

外层每完成一轮，整行已处理；内层不变量是当前行 [0,col) 已输出。若用一个 k 同时作为行列，方阵小样例可能掩盖错误，非方阵测试更有诊断价值。

四个故障对应四个证明缺口

故障实验先预测：哪个访问越界、哪个条件不变、EOF 后哪个旧值被复用、哪个维度首先超界。运行时可配合 sanitizer 和迭代上限，但工具报告只是定位证据，根因仍是边界/推进契约缺失。

三步验收一个循环

小结

• 关系表达式定义继续状态集合，操作数类型和半开区间决定边界是否正确
• for、while、do while 和范围 for 表达不同控制契约，应选择最清楚暴露不变量与推进的形式
• 循环不变量连接已处理和未处理部分，推进量证明终止，退出后置条件说明最终结果
• 文本循环必须由读取成功驱动，EOF 与业务哨兵是不同退出原因
• 嵌套循环逐维证明边界，二维总元素数不能替代行列下标契约

名词解释