一种用于循环程序形式化验证的划分归纳方法

摘要

为了提高软件的可靠性,人们一直在形式化验证和软件测试两个方面进行不懈的努力。本文利用划分测试中的自动分割替代技术,针对循环程序的输入域,提出了一种划分算法,并在此算法的结果上建立一种划分归纳方法,它能简化循环程序的形式化验证过程。