Computer Engineering and Applications ›› 2009, Vol. 45 ›› Issue (8): 50-54.DOI: 10.3778/j.issn.1002-8331.2009.08.016

• 研究、探讨 • Previous Articles     Next Articles

PAR method and loop invariants’ category theory semantic

QU Wen-jian1,2,XUE Jin-yun3,4   

  1. 1.Department of Information Management,College of Information and Engineering,Nanchang University,Nanchang 330031,China
    2.College of Information Management,Jiangxi University of Finance and Economics,Nanchang 330013,China
    3.College of Computer Information and Engineering,Jiangxi Normal University,Nanchang 330027,China
    4.Key Laboratory for Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100080,China
  • Received:2008-01-25 Revised:2008-05-09 Online:2009-03-11 Published:2009-03-11
  • Contact: QU Wen-jian

PAR方法和循环不变式的范畴语义

屈文建1,2,薛锦云3,4   

  1. 1.南昌大学 计算机信息工程学院 信息管理系,南昌 330031
    2.江西财经大学 信息管理学院,南昌 330013
    3.江西师范大学 计算机信息工程学院,南昌 330027
    4.中国科学院 软件研究所 计算机科学重点实验室,北京 100080
  • 通讯作者: 屈文建

Abstract: Category theory promotes a high degree of confidence in design,proof and derivation of algorithmic program.It is differentiated from most other methods in that it is based on a rigorous mathematical foundation.The PAR method is a unified approach for developing efficient algorithmic programs.The loop invariant is the pivotal technology in loop program.This paper discusses a few idea and methods for applying category theory in PAR method and loop programming.Many loop invariants can be expressed in the form of the fixed point of a predicate universal function while weakest precondition is least fixed point and explained in the view of category theory.

Key words: loop invariant, least fixed point, category theory, PAR method

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

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