北京交通大学学报
北京交通大學學報
북경교통대학학보
JOURNAL OF NORTHERN JIAOTONG UNIVERSITY
2012年
2期
1-7
,共7页
程序验证%不变式生成%符号计算%吴方法
程序驗證%不變式生成%符號計算%吳方法
정서험증%불변식생성%부호계산%오방법
在并发程序的分析及验证过程中,不变式起着至关重要的作用,为了提高非线性不变式自动生成算法的效率及通用性,基于将非线性不变式生成问题转换为数值约束求解问题的思想,提出通过检验根理想的从属关系方法使算法具备处理通用代数变迁系统的能力；建立了基于吴方法的非线性不变式自动生成算法,该算法不使用加强的归纳条件,并可以直接处理约束方程.
在併髮程序的分析及驗證過程中,不變式起著至關重要的作用,為瞭提高非線性不變式自動生成算法的效率及通用性,基于將非線性不變式生成問題轉換為數值約束求解問題的思想,提齣通過檢驗根理想的從屬關繫方法使算法具備處理通用代數變遷繫統的能力；建立瞭基于吳方法的非線性不變式自動生成算法,該算法不使用加彊的歸納條件,併可以直接處理約束方程.
재병발정서적분석급험증과정중,불변식기착지관중요적작용,위료제고비선성불변식자동생성산법적효솔급통용성,기우장비선성불변식생성문제전환위수치약속구해문제적사상,제출통과검험근이상적종속관계방법사산법구비처리통용대수변천계통적능력；건립료기우오방법적비선성불변식자동생성산법,해산법불사용가강적귀납조건,병가이직접처리약속방정.
