name:第五部分：程序验证的推理规则 scene1 title:程序验证的过程 scene1 content:程序验证通常有四个步骤：1. 明确初始和最终断言p和q。2. 将程序分解成小的片段。3. 使用推理规则证明每个片段的正确性。4. 组合起来，证明整个程序的正确性。 scene2 title:组合规则 (Composition Rule) scene2 content:对于顺序执行的两个程序段S1和S2，我们可以使用组合规则。如果我们已经证明了p{S1}q和q{S2}r，那么我们可以推断出p{S1; S2}r。也就是说，S1的后置条件q成为了S2的前置条件。 scene3 title:验证条件语句：if-then scene3 content:如何验证一个 'if condition then S' 形式的语句？我们需要证明两种情况：1. 当p和condition都为真时，执行S后，q为真。2. 当p为真但condition为假时，S不执行，此时q仍然为真。 scene4 title:if-then 推理规则 scene4 content:这两种情况可以形式化为一条推理规则：如果 (p ∧ condition){S}q 和 (p ∧ ¬condition) → q 都成立，那么我们就可以得出结论 p{if condition then S}q 成立。 scene5 title:if-then 规则示例 scene5 content:我们来验证 'if x > y then y := x'。后置条件是 y ≥ x。情况一：如果x > y为真，程序执行y:=x，执行后y=x，所以y≥x成立。情况二：如果x > y为假，即x≤y，程序不执行，y的值不变，此时y≥x也成立。因此，该语句是正确的。 scene6 title:验证条件语句：if-then-else scene6 content:对于 'if condition then S1 else S2' 语句，我们需要证明：1. 当p和condition为真时，执行S1后q为真。2. 当p为真且condition为假时，执行S2后q为真。 scene7 title:if-then-else 推理规则 scene7 content:其形式化的推理规则是：如果 (p ∧ condition){S1}q 和 (p ∧ ¬condition){S2}q 都成立，那么我们就可以得出结论 p{if condition then S1 else S2}q 成立。 scene8 title:if-then-else 规则示例：绝对值 scene8 content:我们来验证一个计算绝对值的程序。如果x<0，abs:=-x；否则，abs:=x。后置条件是abs=|x|。当x<0时，abs被赋值为-x，根据定义这就是|x|。当x≥0时，abs被赋值为x，根据定义这也是|x|。两种情况都满足后置条件，因此程序正确。