摘要：描述了一種產(chǎn)生循環(huán)不變式主要部分的方法。該方法的基本思想是在每一次循環(huán)條件變化時(shí)記錄下程序變量的值，生成相應(yīng)的跟蹤表，從跟蹤表中獲得程序變量之間的函數(shù)關(guān)系構(gòu)成循環(huán)不變式的主要部分。程序變量之間的函數(shù)關(guān)系則利用遺傳規(guī)劃對(duì)跟蹤表中數(shù)據(jù)執(zhí)行符號(hào)回歸得到。

關(guān)鍵詞：循環(huán)不變式；Hoare邏輯；符號(hào)回歸；遺傳規(guī)劃