一种基于程序正确性证明理论的程序开发方法  

A Developing Method of Programs Based on the Proof Theory of Program Correctness

作　　者：杨庆红[1] 李云清[1] 

机构地区：[1]江西师范大学计算机科学与技术学院,江西南昌330027

出　　处：《计算机应用研究》2001年第2期11-13,共3页Application Research of Computers

基　　金：国家自然科学基金资助项目(69783006和69983003)

摘　　要：程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法，它使得程序的开发和证明同时进行，程序开发完成的同时其正确性亦得以保证。以两个问题的程序开发为例说明了程序的形式推导方法的使用。Formal derivation of programs is a developing method of programs based on the proof theory of program correctness. It can make the proof process of a program be in progress with the development of the program in the meantime so that the program correctness can be ensured while it's development finishes. This paper presents the steps of the formal derivation method of programs by the development of two problems.

关 键 词：程序的形式推导方法 程序规范 循环不变式 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]