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

無效

• 申請號: 201310474324.4
• 申請日: 2013-10-12
• 公開（公告）號: CN103488571A
• 公開（公告）日: 2014-01-01
• 發明（設計）人: 吳明暉;呂嘉;顏暉;應晶;陳天洲
• 申請（專利權）人: 浙江大學城市學院
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 杭州求是專利事務所有限公司 33200
• 代理人: 杜軍

1.一種混合驗證JavaScript程序正確性的方法，其特征在于包括以下步驟：

步驟1.判斷程序組件是否包含動態語法特性，若有，則程序組件劃分為靜態部分和動態部分兩大部分；

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

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

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

P::=x‾=e‾|P1;P2|P1<P2|if c thenP1elseP2|if c then P|while c do P]]>

其中：表示一組程序變量x₁....,x_n組成的向量，表示一組表達式e₁,...,e_n組成的向量，順序執行表示成P₁;P₂，對于程序代碼P₁和P₂,其中程序代碼P₁先執行,然后程序代碼P₂執行；動態部分插入靜態部分表示成P₁＜P₂:對于程序代碼

P₁和P₂,其中程序代碼P₁是靜態代碼,程序代碼P₂是動態代碼；

步驟4.步驟4.針對靜態部分的程序規約，建立開放系統的有限狀態機模型，其中靜態部分抽象成開放系統的內部遷移，動態部分抽象成開放系統的外部遷移，外部遷移對開放系統的影響必須確保系統的正確性，并使用模型檢測工具驗證系統的正確性，如果驗證正確則程序正確，如果發現錯誤則程序驗證錯誤。

2.如權利要求1所述的一種混合驗證JavaScript程序正確性的方法，其特征在于步驟1中所述的靜態部分不包含動態語法特性，使用程序證明方法進行驗證；動態部分使用模型檢測方法進行驗證，靜態動態部分的組合劃分至動態部分，使用程序證明方法進行驗證。

3.如權利要求1所述的一種混合驗證JavaScript程序正確性的方法，其特征在于步驟3中所述的證明規則定義如下：

(1)賦值規則

A(pre?S?rely)

A(pre(x←e)Srely){x=e}sat‾(pre,rely,pre(x←e))]]>

(2)一致性規則

Psat(pre′,rely′,post′),

pre→pre′,

rely→rely′,

post→post′Psat‾(pre,rely,post)]]>

(3)順序組合規則

P₁sat(pre,rely,g),

P2sat‾(g,rely,post)P1;P2sat‾(pre,rely,post)]]>

(4)動態組合規則

P₁sat(pre₁,rely₁,post₁)

P₂sat(pre₂,rely₂,post₂),

A(rely₁?S?rely₁),

rely1→rely2P1<P2sat‾(pre1,rely1,post1)]]>

(5)條件規則

P₁sat(pre∧c,rely,post),

A(pre S rely)if c thenP1elseP2sat‾(pre,rely,post)]]>

P₁sat(pre∧c,rely,post),

A(pre S rely)if c thenP1sat‾(pre,rely,post)]]>

(6)迭代規則

Psat(pre∧c,rely,pre)

A(pre?S?rely)