一種自動生成循環(huán)摘要的方法

　　采用形式化方法證明軟件的正確性，是保障軟件可靠性的有效方法．而對循環(huán)語句的分析與驗證，是形式化證明中的關(guān)鍵對循環(huán)語句的處理一直是程序分析與驗證中的一個難點問題．提出使用循環(huán)語句修改的內(nèi)存和這些內(nèi)存中存放的新值來描述循環(huán)語句的執(zhí)行效果，并將該執(zhí)行效果定義為循環(huán)摘要，同時，提出一種自動生成循環(huán)摘要的方法，可以為操作常用數(shù)據(jù)結(jié)構(gòu)的循環(huán)自動生成循環(huán)摘要，包含嵌套循環(huán)．此外，基于循環(huán)摘要，可以自動生成循環(huán)語句的規(guī)約。包括循環(huán)不變式、循環(huán)的前置條件以及循環(huán)的后置條件．已經(jīng)實現(xiàn)了自動生成循環(huán)摘要以及循環(huán)規(guī)約的方法，并將它們集成到驗證工具Accumulator中．實驗結(jié)果表明，該方法可以有效地生成循環(huán)摘要，并生成多種類型的規(guī)約，從而輔助軟件程序的形式化證明，提高驗證的自動化程度和效率，減輕驗證人員的負(fù)擔(dān)．
?