CAJ | 학술논문

开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点.本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码.实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性.
개발섭급비선성수거결구산법정서적순배불변식일직시형식화방법적난점.본문사용PAR방법개발순배불변식적신책략,대후서편력이차수문제순배불변식적개발사용체귀정의기술,득도료해문제순배불변식적간단정학적표체형식,간화료산법정서적추도화증명과정;이용PAR평태제공적추상정서설계어언Ap1a중적수거추상궤제,사소득적산법정서결구간길청석차역우증명;최후,사용Dijkstra-Gries표준정서증명법형식증명료해문제적핵심산법정서(지유4행대마),병사용PAR평태장Apla정서전환성정학적C++대마.실례적성공진일보설명PAR방법제공적순배불변식적개발기술대추도화증명비선성수거결구산법정서적유효성.
Developing loop invariants of algorithms containing non-linear data structure is generally regarded as a difficult problem. In this paper, new strategies for developing loop invariant are introduced, and an exact and simple loop invariant of the non-recursive postorder binary-tree traversal algorithm is worked out by adopting the recursive definition technique of loop invariants and ideas of partition-and-recur. The approach considerably simplifies the process of derivation and proof of the non-recursive algorithm and avoids the blindness of developing the loop invariant. Using datatype abstraction of Apla language, which is a part of PAR, the result algorithmic program is pretty concise and easy to be proved. Finally, the core algorithm (just 4 lines in Apla) is successfully proved by Dijkstra-Gries standard proving technique, and the abstract program is transformed into C++ program by PAR platform. It is demonstrated that the recursive definition technique of loop invariant is feasible and effective for deriving and proving non-linear data structure algorithms.