【摘要】 通过证明程序规约的方法可构造相应程序．但对“难题”和无证明的规约，无法使用这种方法构造程序．另一方面，如果可构造程序规约的验证程序，则可把这种程序看成该规约的程序．本文讨论了程序规约的验证程序的构造方法，作为研究程序自动化的一种途径．更多还原

【Abstract】 Programs can be synthesized by proving program specifications.However, some problems, which are hardly to be proved or have no proof, can not be manipulated smoothly in this way. On the other hand, if a verification program of the specification can be constructed, it can be regarded as the required program. This paper discusses how to construct a verification program for the given specification,so as to study a new kind of automatic programming method.更多还原