结构化程序正确性证明：重复递归引理解析

“程序设计方法学基本理论.ppt” 在程序设计方法学中，正确性证明是确保代码功能正确性的重要手段。本课内容主要聚焦于结构化程序的正确性证明，特别是通过序列、条件和循环这三种基本结构来分析和验证程序的正确性。结构化编程强调将复杂的控制流程分解为这些基本结构，以便更易于理解和验证。 重复递归引理是正确性证明中的一个重要概念，它涉及到如何证明循环程序的正确性。引理的核心思想是将循环转换为递归的形式，从而使证明过程简化。以下是三个关键的重复递归引理： 1. **引理1：while-do的正确性定理** 假设我们有一个程序P，它包含一个while-do循环，并期望它实现函数f。根据引理1，P正确实现f的充要条件是：对于所有输入X属于f的定义域，程序P终止，并且其行为等同于if-then结构，即`if p then g; f`。这里的g是循环体，p是循环的终止条件。 - **必要性**：证明了如果P正确实现f，那么它等价于if-then结构。 - **充分性**：证明了if-then结构的行为可以等价地转换回while-do循环。 2. **引理2：do-until的正确性定理** 对于do-until循环，P正确实现f的充要条件是P终止，且其行为等同于`g; if ~p then f`，其中~p是p的否定，g是循环体。 3. **引理3：do-while-do的正确性定理** 这个引理涉及do-1-g-while-p-do-2-h结构，其正确性条件是P终止，并且行为等同于`g; if p then h; f`。 这些引理表明，循环的正确性可以通过转化成递归形式，结合终止性检查和无循环结构（如序列和选择）的正确性证明来验证。这种转化方法使得复杂循环的验证变得更为直观和可管理。 正确性定理的第二个部分未给出完整信息，但通常会涵盖序列结构（p=g;h）和if-then结构（if p then g else h）的情况。对于序列，函数f应满足输入输出的关系，即f应由g和h的操作组合决定。对于if-then结构，f应根据条件p的真假来应用g或h。 程序设计方法学的基本理论强调正确性证明的重要性，提供了将循环程序转化为等价的非循环结构的方法，从而简化了证明过程。这种方法有助于确保程序的正确执行，减少错误，提高软件质量。