[發(fā)明專利]基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法

在審

• 申請?zhí)枺?/td>: 201910630164.5
• 申請日: 2019-07-12
• 公開（公告）號: CN110377513A
• 公開（公告）日: 2019-10-25
• 發(fā)明（設(shè)計）人: 路紅;史玉石
• 申請（專利權(quán)）人: 南京理工大學(xué)紫金學(xué)院
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 南京知識律師事務(wù)所 32207
• 代理人: 李吉寬

1.基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法，其特征在于，包含以下步驟：

步驟一，對含循環(huán)語句的計算機程序依據(jù)所設(shè)計的自動生成后置條件的算法得到所述循環(huán)語句的后置條件，構(gòu)造上述程序中循環(huán)語句對應(yīng)的Hoare三元組；

步驟二，依據(jù)所述循環(huán)語句的前置條件隨機生成測試數(shù)據(jù)，以這些測試數(shù)據(jù)為循環(huán)變量的初始值運行循環(huán)語句，收集程序狀態(tài)，從而構(gòu)造數(shù)據(jù)集SV；

步驟三，對數(shù)據(jù)集SV中的每一組數(shù)據(jù)，依據(jù)Hoare三元組所定義的關(guān)系進行分類標(biāo)注，形成分類數(shù)據(jù)集；

步驟四，利用所設(shè)計的核向量機KSVM算法對所收集的分類數(shù)據(jù)集進行分類，從而生成候選循環(huán)不變式；

步驟五，利用反證法對生成的候選循環(huán)不變式進行有效性驗證，得到經(jīng)驗證的有效循環(huán)不變式。

2.根據(jù)權(quán)利要求1所述的基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法，其特征在于：步驟一中，所述的自動生成后置條件的算法是通過邊界值分析法計算出循環(huán)次數(shù)，并與循環(huán)語句的前置條件合成得到一些公式集合，并對這些公式集合進行簡化得到后置條件。

3.根據(jù)權(quán)利要求1所述的基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法，其特征在于：步驟二中，所述的依據(jù)循環(huán)語句的前置條件隨機生成測試數(shù)據(jù)是通過隨機方式生成滿足前置條件的數(shù)據(jù)集SP和不滿足前置條件的數(shù)據(jù)集SN，兩種方式構(gòu)造測試數(shù)據(jù)集SV＝SP∪SN。

4.根據(jù)權(quán)利要求3所述的基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法，其特征在于：步驟二中，所述程序狀態(tài)是程序中每個變量名到變量值的映射集合，將所有的程序狀態(tài)作為測試數(shù)據(jù)集SV，依據(jù)循環(huán)條件執(zhí)行有限次循環(huán)語句，并記錄每一次循環(huán)結(jié)束后程序狀態(tài)，組成數(shù)據(jù)集SC，并將數(shù)據(jù)集SC加入到數(shù)據(jù)集SV中，即SV＝SP∪SN∪SC。

5.根據(jù)權(quán)利要求1所述的基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法，其特征在于：步驟三中，所述分類標(biāo)注是指依據(jù)循環(huán)不變式與Hoare三元組中所定義的前置條件、后置條件和循環(huán)體的關(guān)系，將步驟二所定義的數(shù)據(jù)集SV標(biāo)注為：錯誤的數(shù)據(jù)、一定滿足循環(huán)不變式的數(shù)據(jù)、一定不滿足循環(huán)不變式的數(shù)據(jù)和不確定的數(shù)據(jù)。

6.根據(jù)權(quán)利要求5所述的基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法，其特征在于：步驟四中，所述的核支持向量機KSVM算法是一種由徑向基核函數(shù)和線性核函數(shù)復(fù)合而成的多核函數(shù)，以使得線性不可分的數(shù)據(jù)能夠在高維空間進行有效劃分，所述候選循環(huán)不變式是能夠明確劃分步驟三所標(biāo)注的一定滿足循環(huán)不變式的數(shù)據(jù)和一定不滿足循環(huán)不變式的數(shù)據(jù)的分類器。

7.根據(jù)權(quán)利要求1所述的基于機器學(xué)習(xí)的循環(huán)不變式自動生成方法，其特征在于：步驟五中，所述有效性驗證是對候選循環(huán)不變式取反，判斷前置條件或后置條件是否存在存在滿足候選循環(huán)不變式范圍之外的數(shù)據(jù)，如果有則為無效候選不變式，否則為有效循環(huán)不變式。