[發(fā)明專利]一種基于中間語言的形式化規(guī)約語言簡化方法

有效

• 申請?zhí)枺?/td>: 201911328421.6
• 申請日: 2019-12-20
• 公開（公告）號: CN111124485B
• 公開（公告）日: 2023-03-10
• 發(fā)明（設(shè)計）人: 李昂;曾惟如;晏昃暉;楊拯;唐琴;錢偉中
• 申請（專利權(quán)）人: 成都互誠在線科技有限公司;電子科技大學(xué)
• 主分類號: G06F8/72
• 分類號: G06F8/72
• 代理公司: 成都君合集專利代理事務(wù)所(普通合伙) 51228
• 代理人: 尹玉

本發(fā)明公開了一種基于中間語言的形式化規(guī)約語言簡化方法，將應(yīng)用程序轉(zhuǎn)化為中間語言程序，然后將中間語言程序映射為Lolisa語言程序；所述中間語言程序包括類型finitpar_type和結(jié)構(gòu)list_pars，采用類型finitpar_type將參數(shù)形式化為Type類型，采用結(jié)構(gòu)list_pars將形式化參數(shù)列表整合為list類型。本發(fā)明將應(yīng)用程序轉(zhuǎn)化為中間語言程序，中間語言將簡化形式化語言的語法，然后根據(jù)中間語言和底層的Lolisa語言的轉(zhuǎn)換關(guān)系，將中間語言程序轉(zhuǎn)化為Lolisa編寫的形式化程序。本發(fā)明簡化了形式化語言的數(shù)據(jù)類型和文法規(guī)則，提高了形式化驗證的用戶友好度。

技術(shù)領(lǐng)域

本發(fā)明屬于計算機應(yīng)用的技術(shù)領(lǐng)域，具體涉及一種基于中間語言的形式化規(guī)約語言簡化方法。

背景技術(shù)

隨著軟件系統(tǒng)越來越復(fù)雜，軟件開發(fā)的成本也不斷提升，使得軟件測試越來越重要。現(xiàn)有的測試方法主要有傳統(tǒng)的用例測試，通過執(zhí)行大量的測試用例發(fā)現(xiàn)程序存在的漏洞，這一方法需要大量的人工編寫測試用例，且無法覆蓋所有的程序代碼。

基于Coq形式化符號執(zhí)行虛擬機^[2]（formal symbolic process virtualmachine，F(xiàn)SPVM）以及可擴展的形式化語言Lolisa能夠?qū)Τ绦蜃詣有问交：万炞C（Yang Z,Lei H.Formal Process Virtual Machine for Smart Contracts Verification[J].International Journal of Performability Engineering,2018）。應(yīng)用程序被等價的翻譯為由形式化高階語言Lolisa描述的形式化程序，該程序由形式化驗證解釋器解釋執(zhí)行并且改變形式化內(nèi)存狀態(tài)，在這一過程中由Coq的形式化內(nèi)核來進行執(zhí)行和驗證，最終的程序執(zhí)行結(jié)果將和預(yù)先給出的后置條件進行對比，從而判斷程序是否存在漏洞。

現(xiàn)階段，規(guī)約化語言Lolisa的語法較為復(fù)雜，使其難以廣泛實際應(yīng)用。Lolisa的絕大多數(shù)文法有四層語法構(gòu)成：語句層、表達式層、值層以及類型層。語句層的文法直接形成形式化程序，語句層在表達式層之上構(gòu)建；表達式層和值層都遵循GADTs規(guī)則，使之都需要類型層來構(gòu)成。同時表達式層需要值層構(gòu)造復(fù)雜的對象，表達式直接的或者通過構(gòu)建參數(shù)列表作為語句的構(gòu)建單元。參數(shù)列表在表達式層上構(gòu)建，用于函數(shù)相關(guān)的語句中存儲對應(yīng)的參數(shù)，Lolisa為不同的參數(shù)列表分別定義了相應(yīng)的列表類型，使得參數(shù)列表語法相當(dāng)復(fù)雜。

發(fā)明內(nèi)容

本發(fā)明的目的在于提供一種基于中間語言的形式化規(guī)約語言簡化方法，旨在解決上述問題，簡化形式化語言的數(shù)據(jù)類型和文法規(guī)則，以提高形式化驗證方法的用戶友好度。

本發(fā)明主要通過以下技術(shù)方案實現(xiàn)：一種基于中間語言的形式化規(guī)約語言簡化方法，將應(yīng)用程序轉(zhuǎn)化為中間語言程序，然后將中間語言程序映射為Lolisa語言程序；所述中間語言程序包括類型finitpar_type和結(jié)構(gòu)list_pars，采用類型finitpar_type將參數(shù)形式化為Type類型，采用結(jié)構(gòu)list_pars將形式化參數(shù)列表整合為list類型。

為了更好地實現(xiàn)本發(fā)明，進一步的，主要包括以下步驟：

步驟S1：使用新類型finitpar_type整合用于構(gòu)建參數(shù)列表的Lolisa表達式，形式化源碼中的參數(shù)；

步驟S2：將形式化參數(shù)組織為統(tǒng)一的list類型的形式化參數(shù)列表，將源碼中的參數(shù)列表轉(zhuǎn)化為list_pars的四元組，list_pars的元素用于存儲不同類型的形式化參數(shù)列表；

步驟S3：在語句中嵌入相對應(yīng)的取元素操作，實現(xiàn)取出list_pars中元素的功能；