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

PAR method and loop invariants'category theory semantic

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

Category theory promotes a high degree of confidence in design,proof and derivation of algorithmic program.It is dif- ferentiated 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.