随着信息技术的不断发展，软件系统的正确性越来越得到人们的关注。程序验证是保证软件系统正确性的一个重要手段。大多数人的关注点放在了软件测试与形式化验证两个方面，且在这两方面中都取得了丰硕的成果。然而，由于软件测试与形式化验证各有其利弊，故近几年来，越来越多的研究人员开始尝试将两种技术结合起来共同提高软件的可靠性。就目前看来，大多数人都是将形式化验证的相关思想用于软件测试的过程中，从而进一步确保软件系统的正确性。 本文从相反的方向考虑，利用软件测试中的划分测试技术，采用“自动分割替代”思想，同时结合划分分析，提出一种划分归纳法，用于循环程序的形式化验证。该方法通过将循环程序的输入域分成若干个子域，在每个子域上建立归纳奠基或归纳递推，同时对其进行相关处理(如副作用的消除)，从而自动构造出一种用于定理证明器归纳逻辑的划分归纳法。该归纳法可简化半交互定理证明器中的交互界面，从而使程序验证过程变得更加简单且易操作。同时，本文对该归纳法的良基性和有效性也进行了证明。最后，利用该归纳法的思想，设计出一个小型程序验证系统原型，其主要功能是自动构造归纳假设，且该归纳假设已为最简形式，从而方便接下来的归纳证明过程。该系统原型的实现表明划分归纳法具有一定的实用性。