从上世纪六十年代起,随着大型软件的快速发展,人们对软件质量的要求起来越高,尤其是对软件的正确性要求。计算机界为确保软件质量尤其是软件的高可靠性方面提出了许多新的理论研究,程序正确性证明就是其中之一,程序正确性证明就是采用严格的数学方法评价一个程序是否达到了预定的性能。但是在证明程序正确的过程中由于要涉及大量的数学符号和数学相关理论知识使得程序验证人员需要花费一定的时间和精力去掌握这些知识。而且由于涉及到数学理论即使验证一个很短的程序也需要比较繁琐的验证过程,造成往往证明过程比要证明的程序要复杂很多的情况,这些种种不利条件使得依靠手工去证明程序正确性就可能产生许多不良的后果。为了克服手工对程序进行正确性验证程序所导致的不良后果,许多计算机科学家开始利用机器去自动验证程序来逐步降低人工干预程序验证的过程,最终的目的是将程序正确性验证走向完全自动化。根据Dijkstra的最弱前置谓词理论,对于程序{Q}S{R},如果能证明:Q ==> WP(“S”,R)则能断定程序正确。正是基于此理论,本文研究作为PAR平台的一个辅助工具部分,目标是开发一个自动计算Apla程序的最弱前置谓词的系统,减少Apla程序正确性验证的人工干预,在已知S,R的情况下自动求解出最弱前置谓词。围绕这个宗旨本文做了如下工作:1、在深刻理解了Dijkstra最弱前置谓词的的基础上提出了自动计算APLA语言最弱前置谓词的算法。2、选取了若干Apla程序进行试验,实验结果表明,系统初步实现了自动计算最弱前置谓词的功能。3、尝试将Dijkstra最弱前置谓词自动生成器整合到PAR平台,使其成为PAR的一个辅助工具;能够有效的支持PAR平台。后期的工作包括完善系统的各项功能;进一步提高系统的可靠性和健壮性;加强对复杂性算法和经典数字问题算法的分析和求解。