中文摘要：

为了使开发出的程序更具有可靠性,研究了两种正确性验证的演算方法,Dijkstra的最弱前置谓词变换法和Hoare的公理化方法。针对于Hoare公理化方法证明中的前置条件难以寻找的问题,提出了将这两种演算方法结合使用的方法。对最弱前置谓词变换法的过程进行分析,确定了最弱前置谓词算法的准确性。将最弱前置谓词应用到公理化方法中,即把最弱前置谓词变换法求出的前置谓词作为公理化方法的前置条件。通过一个具体实例,详细说明了其验证过程,并证明了该方法的有效性。

英文摘要：

To develop a more reliable program, two checking methods about program＇ s varification of correctness are studied, such as Dijkstra＇ s weakest pre-predicate transformer and Hoare＇ s axiomatic approach. Cosidering the difficulities to search pre-condition of Hoare＇ axiomatic approach, an idea of combing these two methods is proposed. Firstly, process of weakest-predicate transformer is analyed, and the accurary of weakest pre-predicate is confirmed. Then, the weakest pre-predicate is applied into axiomatic approach- the predicate of the weakest pre-predicate transfer is served as the precondition of the axiomtics. Finally, the process is specified through a real design instance and efficency of the presented method is demostrated.