[發(fā)明專利]一種混合驗證JavaScript程序正確性的方法

無效

• 申請?zhí)枺?/td>: 201310474324.4
• 申請日: 2013-10-12
• 公開（公告）號: CN103488571A
• 公開（公告）日: 2014-01-01
• 發(fā)明（設(shè)計）人: 吳明暉;呂嘉;顏暉;應(yīng)晶;陳天洲
• 申請（專利權(quán)）人: 浙江大學(xué)城市學(xué)院
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 杭州求是專利事務(wù)所有限公司 33200
• 代理人: 杜軍

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

本發(fā)明屬于計算機軟件驗證領(lǐng)域，特別是涉及一種混合驗證JavaScript程序正確性的方法。

背景技術(shù)

JavaScript語言是一種廣泛應(yīng)用于互聯(lián)網(wǎng)應(yīng)用程序的腳本語言，由于支持各種動態(tài)語法特性，JavaScript語言具有很好的表達(dá)能力和靈活性，使用JavaScript語言可以提高軟件系統(tǒng)的開發(fā)效率和開發(fā)速度，提高軟件系統(tǒng)的可讀性和可重用性。

JavaScript語言支持動態(tài)語法特性包括：動態(tài)類型、隱式類型轉(zhuǎn)換、運行時求解和反射等，由于各種動態(tài)語法特性的引入，JavaScript程序很難使用傳統(tǒng)的程序證明和模型檢測(model?checking)方法進行驗證。

形式化方法是借助數(shù)學(xué)的方法來研究計算機科學(xué)中的有關(guān)問題。從廣義角度，形式化方法是軟件開發(fā)過程中分析、設(shè)計及實現(xiàn)的系統(tǒng)工程方法。狹義地，形式化方法是軟件規(guī)格和驗證的方法，形式化驗證的主要技術(shù)包括模型檢驗和定理證明。

模型檢驗是一種基于有限狀態(tài)模型并檢驗該模型的期望特性的技術(shù)。模型檢驗主要適用于有窮狀態(tài)系統(tǒng)，其優(yōu)點是完全自動化并且驗證速度快；并且，模型檢驗可用于系統(tǒng)部分規(guī)格，即對于只給出了部分規(guī)格的系統(tǒng)，通過搜索也可以提供關(guān)于已知部分正確性的有用信息；此外，當(dāng)所檢驗的性質(zhì)未被滿足時，將終止搜索過程并給出反例，這種信息常常反映了系統(tǒng)設(shè)計中的細(xì)微失誤，因而對于用戶排錯有極大的幫助。模型檢驗方法的一個缺陷是“狀態(tài)爆炸問題”，即隨著所要檢驗的系統(tǒng)的規(guī)模增大，模型檢驗算法所需的時間/空間開銷往往呈指數(shù)增長，因而限制了其實際使用范圍。

定理證明采用邏輯公式來規(guī)格系統(tǒng)及其性質(zhì)，其中的邏輯由一個具有公理和推理規(guī)則的形式化系統(tǒng)給出，進行定理證明的過程就是應(yīng)用這些公理或推理規(guī)則來證明系統(tǒng)具有某些性質(zhì)。不同于模型檢驗，定理證明可以處理無限狀態(tài)空間問題。定理證明系統(tǒng)可以分為自動和交互式兩種類型。自動定理證明系統(tǒng)是通用搜索過程，在解決各種組合問題中比較成功；交互式定理證明系統(tǒng)需要與用戶進行交互，要求用戶能提供驗證中創(chuàng)造性最強部分（建立斷言等）的工作，因而其效率較低，較難用于大系統(tǒng)的驗證。

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

本發(fā)明目的是針對JavaScript的動態(tài)語法特性，針對模型檢測方法和程序證明方法各自的不足，提供一種混合驗證JavaScript程序正確性的方法。

本發(fā)明解決其技術(shù)問題所采取的技術(shù)方案包括以下步驟：

步驟1.判斷程序組件是否包含動態(tài)語法特性，若有，則程序組件劃分為靜態(tài)部分和動態(tài)部分兩大部分：靜態(tài)部分不包含動態(tài)語法特性，使用程序證明方法進行驗證；動態(tài)部分使用模型檢測方法進行驗證，靜態(tài)動態(tài)部分的組合劃分至動態(tài)部分，使用程序證明方法進行驗證。

步驟2.將劃分后的靜態(tài)部分通過程序規(guī)約方法進行規(guī)約，使用開放時態(tài)邏輯對JavaScript程序進行形式化規(guī)約；開放時態(tài)邏輯擴展計算樹邏輯，具體的通過引入新的路徑算子和時態(tài)算子，擴展計算樹邏輯的描述和推理能力,開放時態(tài)邏輯的語法使用BNF范式描述如下:

其中p屬于命題公式集合；使用開放時態(tài)邏輯形式化規(guī)約JavaScript程序正確性：對于一段JavaScript程序代碼P，程序規(guī)約表示成(pre,rely,post)：其中pre是程序代碼P執(zhí)行前的前置條件，rely是程序代碼P執(zhí)行過程中的依賴條件，post是程序代碼P執(zhí)行完成后的后置條件，其中前置條件和依賴條件是程序代碼P正確執(zhí)行的假設(shè)，后置條件是程序代碼P正確執(zhí)行的承諾。

步驟3.使用程序證明方法驗證靜態(tài)部分和靜態(tài)動態(tài)組合的正確性，證明系統(tǒng)包括一個核心語言和一組證明規(guī)則。核心語言抽象描述JavaScript程序，證明系統(tǒng)中的程序證明方法定義如下：