[發明專利]基于后置條件的循環不變式自動生成方法

在審

• 申請號: 202011276827.7
• 申請日: 2020-11-16
• 公開（公告）號: CN112527629A
• 公開（公告）日: 2021-03-19
• 發明（設計）人: 路紅;廖龍龍;史玉石;劉紅英
• 申請（專利權）人: 南京理工大學紫金學院
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06N20/10
• 代理公司: 南京銳恒專利代理事務所(普通合伙) 32506
• 代理人: 劉佳偉

1.基于后置條件的循環不變式自動生成方法，其特征在于：包含以下步驟：

步驟一，根據循環語句塊構造初始候選不變式CanInv，在霍爾邏輯驗證規則中后置條件是循環不變式的弱化形式，借助這一邏輯關系依據循環語句塊的后置條件構造候選不變式CanInv；

步驟二，構造一個不變式驗證器以驗證候選不變式CanInv是否有效，若CanInv能通過程序驗證，則該程序的可驗證的循環不變式Inv已生成，即Inv＝CanInv；若CanInv不能通過驗證，則得到反例數據并將其加入樣本數據集；

步驟三，為更新步驟二中不能通過驗證的候選循環不變式CanInv，生成樣本數據集SD；

步驟四，標注步驟三中所生成的樣本數據集SD，利用核支持向量機方法在這些標注過的樣本數據集SD上學習一個分類器；

步驟五，利用步驟四所生成的分類器更新候選不變式CanInv，若更新后的候選循環不變式CanInv無法通過驗證，則返回步驟二進行下一輪循環，進行候選不變式CanInv的迭代更新。

2.根據權利要求1所述的基于后置條件的循環不變式自動生成方法，其特征在于：在步驟一中對循環語句塊構造初始候選不變式CanInv是利用后置條件與循環不變式的邏輯關系，將后置條件做等價線性變換或多項式不等式變換從而建立一個初始候選不變式。

3.根據權利要求1所述的基于后置條件的循環不變式自動生成方法，其特征在于：步驟二中所述不變式驗證器既可以用來驗證單層循環不變式的有效性也可以用來驗證嵌套循環不變式的有效性。

4.根據權利要求3所述的基于后置條件的循環不變式自動生成方法，其特征在于：單層循環的不變式驗證是采用反證法，驗證規則如下：

5.根據權利要求3所述的基于后置條件的循環不變式自動生成方法，其特征在于：兩層嵌套循環的不變式驗證規則如下：

P→Inv， (1)

{Inv∧C}{Body1∧Inv_inn∧Body2}{Inv} (2)

P_inn∧Inv→Inv_inn (4)

{Inv_inn∧C_inn}{Body_inn}{Inv_inn} (5)

其中，P_inn、Inv_inn、C_inn、Body_inn、Q_inn分別表示內層循環的前置條件、循環不變式、循環條件、循環體和后置條件。

6.根據權利要求1所述的基于后置條件的循環不變式自動生成方法，其特征在于：步驟二中，所述得到反例數據是指利用可滿足性理論的求解技術計算出不能通過有效性驗證的循環不變式的反例數據，并采集這些反列數據作為分類樣本數據，作為下一輪更新候選循環不變式的依據。

7.根據權利要求1所述的基于后置條件的循環不變式自動生成方法，其特征在于：步驟三中，生成的樣本數據集SD包括，(1)在步驟二中生成的候選不變式的邊界上選取的樣本數據；(2)依據循環前置條件P生成滿足P和不滿足P的樣本數據，以及將滿足P的樣本數據作為循環輸入，運行循環語句所得到的新樣本數據；(3)步驟二中所生成的反例數據。

8.根據權利要求1所述的基于后置條件的循環不變式自動生成方法，其特征在于：步驟四中，所述標注所生成的樣本數據集SD是指依據程序驗證規則中程序的前置條件、后置條件和循環體，將步驟三所生成的數據集SD標注為三類：正樣本數據、反例樣本數據和不確定的樣本數據。

9.根據權利要求1所述的基于后置條件的循環不變式自動生成方法，其特征在于：步驟五中，所述的利用步驟四所生成的KSVM分類器更新候選不變式CanInv是將步驟四中所學習到的KSVM分類器作為新的候選不變式，并繼續返回步驟二中驗證其有效性，以判斷該候選不變式是否為可驗證的循環不變式，從而決定是否需要進行下一輪求解。