循环不变式

June 3, 2022

定义 #

循环不变式： 循环的每次迭代中，始终为 true 的断言

\( (P \land condition) \{ S \} P \)，即 \(P\) 为循环不变式

证明循环语句正确的步骤 #

1. 猜测 \(P\) 为循环不变式
2. 证明 \(P\) 为循环不变式
3. 证明程序会终止
4. 证明程序终止时 \(P \land \neg condition \) 为 \( T \)