计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2009年
8期
50-54
,共5页
循环不变式%最小不动点%范畴论%PAR方法
循環不變式%最小不動點%範疇論%PAR方法
순배불변식%최소불동점%범주론%PAR방법
范畴论对理解程序规约及程序设计和正确性证明十分有用.PAR方法则是建立在严格的数学基础之上的一种统一的算法程序设计方法.循环不变式在循环算法程序的设计中至关重要.使用格理论和范畴论作为工具对PAR方法建立一个理论框架,并对其用范畴论的概念加以解释,从而使得PAR有更强的理论基础.在此基础上引入不动点原理深入刻划循环不变式的含义,循环不变式可以表示为谓词泛函的最小不动点,并从范畴论的角度解释该过程.
範疇論對理解程序規約及程序設計和正確性證明十分有用.PAR方法則是建立在嚴格的數學基礎之上的一種統一的算法程序設計方法.循環不變式在循環算法程序的設計中至關重要.使用格理論和範疇論作為工具對PAR方法建立一箇理論框架,併對其用範疇論的概唸加以解釋,從而使得PAR有更彊的理論基礎.在此基礎上引入不動點原理深入刻劃循環不變式的含義,循環不變式可以錶示為謂詞汎函的最小不動點,併從範疇論的角度解釋該過程.
범주론대리해정서규약급정서설계화정학성증명십분유용.PAR방법칙시건립재엄격적수학기출지상적일충통일적산법정서설계방법.순배불변식재순배산법정서적설계중지관중요.사용격이론화범주론작위공구대PAR방법건립일개이론광가,병대기용범주론적개념가이해석,종이사득PAR유경강적이론기출.재차기출상인입불동점원리심입각화순배불변식적함의,순배불변식가이표시위위사범함적최소불동점,병종범주론적각도해석해과정.