文献类型：期刊文章

作　　者：屈文建[1,2] 薛锦云[3,4]

机构地区：[1]南昌大学计算机信息工程学院信息管理系,南昌330031 [2]江西财经大学信息管理学院,南昌330013 [3]江西师范大学计算机信息工程学院,南昌330027 [4]中国科学院软件研究所计算机科学重点实验室,北京100080

出　　处：《计算机工程与应用》

基　　金：国家自然科学基金No.60273092~~

年　　份：2009

卷　　号：45

期　　号：8

起止页码：50-54

语　　种：中文

收录情况：AJ、BDHX、BDHX2008、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、IC、INSPEC、JST、RCCSE、ZGKJHX、核心刊

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

关 键 词：循环不变式 最小不动点  范畴论 PAR方法

分 类 号：TP311]