[發明專利]一種混合驗證JavaScript程序正確性的方法無效
| 申請號: | 201310474324.4 | 申請日: | 2013-10-12 |
| 公開(公告)號: | CN103488571A | 公開(公告)日: | 2014-01-01 |
| 發明(設計)人: | 吳明暉;呂嘉;顏暉;應晶;陳天洲 | 申請(專利權)人: | 浙江大學城市學院 |
| 主分類號: | G06F11/36 | 分類號: | G06F11/36 |
| 代理公司: | 杭州求是專利事務所有限公司 33200 | 代理人: | 杜軍 |
| 地址: | 310015 浙*** | 國省代碼: | 浙江;33 |
| 權利要求書: | 查看更多 | 說明書: | 查看更多 |
| 摘要: | |||
| 搜索關鍵詞: | 一種 混合 驗證 javascript 程序 正確性 方法 | ||
1.一種混合驗證JavaScript程序正確性的方法,其特征在于包括以下步驟:
步驟1.判斷程序組件是否包含動態語法特性,若有,則程序組件劃分為靜態部分和動態部分兩大部分;
步驟2.將劃分后的靜態部分通過程序規約方法進行規約,使用開放時態邏輯對JavaScript程序進行形式化規約;開放時態邏輯擴展計算樹邏輯,具體的通過引入新的路徑算子和時態算子,擴展計算樹邏輯的描述和推理能力,開放時態邏輯的語法使用BNF范式描述如下:
其中p屬于命題公式集合;使用開放時態邏輯形式化規約JavaScript程序正確性:對于一段JavaScript程序代碼P,程序規約表示成(pre,rely,post):其中pre是程序代碼P執行前的前置條件,rely是程序代碼P執行過程中的依賴條件,post是程序代碼P執行完成后的后置條件,其中前置條件和依賴條件是程序代碼P正確執行的假設,后置條件是程序代碼P正確執行的承諾;
步驟3.使用程序證明方法驗證靜態部分和靜態動態組合的正確性,證明系統包括一個核心語言和一組證明規則;核心語言抽象描述JavaScript程序,證明系統中的程序證明方法定義如下:
其中:表示一組程序變量x1....,xn組成的向量,表示一組表達式e1,...,en組成的向量,順序執行表示成P1;P2,對于程序代碼P1和P2,其中程序代碼P1先執行,然后程序代碼P2執行;動態部分插入靜態部分表示成P1<P2:對于程序代碼
P1和P2,其中程序代碼P1是靜態代碼,程序代碼P2是動態代碼;
步驟4.步驟4.針對靜態部分的程序規約,建立開放系統的有限狀態機模型,其中靜態部分抽象成開放系統的內部遷移,動態部分抽象成開放系統的外部遷移,外部遷移對開放系統的影響必須確保系統的正確性,并使用模型檢測工具驗證系統的正確性,如果驗證正確則程序正確,如果發現錯誤則程序驗證錯誤。
2.如權利要求1所述的一種混合驗證JavaScript程序正確性的方法,其特征在于步驟1中所述的靜態部分不包含動態語法特性,使用程序證明方法進行驗證;動態部分使用模型檢測方法進行驗證,靜態動態部分的組合劃分至動態部分,使用程序證明方法進行驗證。
3.如權利要求1所述的一種混合驗證JavaScript程序正確性的方法,其特征在于步驟3中所述的證明規則定義如下:
(1)賦值規則
A(pre?S?rely)
(2)一致性規則
Psat(pre′,rely′,post′),
pre→pre′,
rely→rely′,
(3)順序組合規則
P1sat(pre,rely,g),
(4)動態組合規則
P1sat(pre1,rely1,post1)
P2sat(pre2,rely2,post2),
A(rely1?S?rely1),
(5)條件規則
P1sat(pre∧c,rely,post),
P1sat(pre∧c,rely,post),
(6)迭代規則
Psat(pre∧c,rely,pre)
A(pre?S?rely)
該專利技術資料僅供研究查看技術是否侵權等信息,商用須獲得專利權人授權。該專利全部權利屬于浙江大學城市學院,未經浙江大學城市學院許可,擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作,請聯系【客服】
本文鏈接:http://www.szxzyx.cn/pat/books/201310474324.4/1.html,轉載請聲明來源鉆瓜專利網。





