基于遺傳規劃尋找循環不變式的方法

摘要：描述了一種產生循環不變式主要部分的方法。該方法的基本思想是在每一次循環條件變化時記錄下程序變量的值，生成相應的跟蹤表，從跟蹤表中獲得程序變量之間的函數關系構成循環不變式的主要部分。程序變量之間的函數關系則利用遺傳規劃對跟蹤表中數據執行符號回歸得到。

關鍵詞：循環不變式；Hoare邏輯；符號回歸；遺傳規劃