论文部分内容阅读
范畴论对理解程序规约及程序设计和正确性证明十分有用。PAR方法则是建立在严格的数学基础之上的一种统一的算法程序设计方法。循环不变式在循环算法程序的设计中至关重要。使用格理论和范畴论作为工具对PAR方法建立一个理论框架，并对其用范畴论的概念加以解释，从而使得PAR有更强的理论基础。在此基础上引入不动点原理深入刻划循环不变式的含义。循环不变式可以表示为谓词泛函的最小不动点，并从范畴论的角度解释该过程。