论文部分内容阅读
循环不变式在算法程序的设计及形式推导和证明中有重要作用。该文指出Ｄｉｊｋｓｔｒａ－Ｇｒｉｅｓ标准循环不变式开发策略存在的局限性，为证明现有程序正确和开发新的算法程序分别提出了两种新的循环不变式开发策略。新策略利用递推用工具，将动态规划法，贪心法，分而治之法等行之有效的算法设计方法统一于问题求解序列的递推关系中，使对一类复杂算法程序的形式推导和证明成为可能，并以实例说明新策略的作用方法和优点。（本刊录）