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

A Partition Induction for the Formal Verification of Loop Programs

作　　者：钟杨[1] 宋国新[1] 计春雷[1,2] 

机构地区：[1]华东理工大学信息科学与工程学院,上海200237 [2]上海电机学院,上海200240

出　　处：《华东理工大学学报（自然科学版）》2008年第6期834-836,共3页Journal of East China University of Science and Technology

基　　金：国家自然科学基金(60473055)

摘　　要：为了提高软件的可靠性,人们一直在形式化验证和软件测试两个方面进行不懈的努力。本文利用划分测试中的自动分割替代技术,针对循环程序的输入域,提出了一种划分算法,并在此算法的结果上建立一种划分归纳方法,它能简化循环程序的形式化验证过程。In order to improve software reliability, an unremitting effort has been made on researching fields of formal verification and software test. By using the automatic partition technique in partition test, this paper presents a partition algorithm and constructs a partition induction based on the results that the algorithm generates. This partition induction can simplify the process of formal verification on a loop procedure.

关 键 词：软件可靠性 形式化验证 划分算法 划分归纳方法 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]