摘要
本文形式地描述了一种证明程序能够正确地进行计算的方法。为了做到这一点，这里给出了一个程序及其执行的抽象模型。然后相对于这一模型给出了程序正确性和程序正确性证明的方法。
This paper formally describes a method for proving that programs will execute correctly ln order to do this,an abstract model for a program and its execution is give.Then,correctness of programs and proofs of correctness of programs are defined with respect to that model.
出处
《大电机技术》
北大核心
1998年第3期18-22,共5页
Large Electric Machine and Hydraulic Turbine
关键词
程序证明
程序正确性
程序设计方法学
program proof program correctness programming methodology abstract model
