name:第六部分：使用循环不变量验证循环 scene1 title:验证循环的挑战 scene1 content:验证带有循环的程序，比如 'while condition do S'，是程序验证中最具挑战性的部分，因为我们不知道循环会执行多少次。 scene2 title:循环不变量 (Loop Invariant) scene2 content:为了解决这个问题，我们引入了“循环不变量”的概念。循环不变量是一个断言p，它在循环的每一次迭代之前和之后都保持为真。形式化地，如果(p ∧ condition){S}p成立，那么p就是一个循环不变量。 scene3 title:迭代规则 (Rule of Iteration) scene3 content:基于循环不变量，我们有了迭代规则：如果p是一个循环不变量，那么我们可以推断出 p{while condition S}(¬condition ∧ p)。这意味着，如果循环开始前p为真，那么当循环结束时（此时condition为假），p仍然为真。 scene4 title:实例：阶乘程序 scene4 content:我们来验证一个计算n的阶乘的程序。程序中有一个while循环，条件是 i < n。我们需要找到一个循环不变量来证明程序最终能得到 fact = n!。 scene5 title:寻找循环不变量 scene5 content:对于阶乘程序，一个合适的循环不变量p是 '(fact = i!) ∧ (i ≤ n)'。这个断言包含了我们想追踪的状态（fact和i的关系）以及循环能够最终终止的条件。 scene6 title:证明p是循环不变量 scene6 content:我们需要证明在循环体执行前后，p都保持为真。假设在某次循环开始时，p和循环条件i<n都为真。循环体内，i变成i+1，fact变成fact*(i+1)。根据假设，新fact等于(i+1)!，新i小于等于n。所以p在循环体执行后仍然为真。 scene7 title:使用迭代规则证明正确性 scene7 content:证明分为三步：1. 证明循环开始前，p为真。在程序初始化后，i=1, fact=1，此时p成立。2. 应用迭代规则，当循环结束时，i<n为假且p为真。这意味着i=n且fact=i!，即fact=n!。3. 证明循环会终止。因为i每次循环都加1，它最终会达到n，使得循环条件为假，从而终止循环。