摘要
程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法，它使得程序的开发和证明同时进行，程序开发完成的同时其正确性亦得以保证。以两个问题的程序开发为例说明了程序的形式推导方法的使用。
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.
出处
《计算机应用研究》
CSCD
北大核心
2001年第2期11-13,共3页
Application Research of Computers
基金
国家自然科学基金资助项目(69783006和69983003)
关键词
程序的形式推导方法
程序规范
循环不变式
Formal derivation method of programs
Program specification
Loop invariant
