[發明專利]一種增量組合JavaScript程序模塊的方法

無效

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

技術領域

本發明屬于計算機軟件驗證領域，特別涉及一種增量組合JavaScript程序模塊的方法。

背景技術

JavaScript語言是一種廣泛應用于互聯網應用程序的腳本語言，JavaScript語言具有很好的表達能力和靈活性，使用JavaScript語言可以提高軟件系統的開發效率和開發速度，提高軟件系統的可讀性和可重用性。

封裝性就是把對象的屬性和行為結合成一個獨立的單位，并盡可能隱蔽對象的內部實現細節，封裝有兩個含義：一是把對象的全部屬性和行為結合在一起，形成一個不可分割的獨立單位。對象的屬性值（除了公有的屬性值）只能由這個對象的行為來讀取和修改；二是盡可能隱蔽對象的內部細節，對外形成一道屏障，與外部的聯系只能通過外部接口實現。

JavaScript語言支持動態語法特性：動態類型、隱式類型轉換、運行時求解和反射等，由于各種動態語法特性的引入，JavaScript程序違反傳統的程序封裝性原則，很難使用傳統的靜態方法進行模塊化分析，支持JavaScript程序的增量組合。

發明內容

本發明的目的是針對現有模塊組合方法的不足，提供一種增量組合JavaScript程序模塊的方法。

本發明解決其技術問題所采用的技術方案如下：

步驟1.將JavaScript程序模塊分為靜態模塊M和動態模塊D：靜態模塊M不包含動態語法特性，支持程序靜態分析；動態模塊D包含動態語法特性，必須在運行時進行檢查；

步驟2.使用信賴-保證方法(rely-guarantee?paradigm)定義靜態模塊M的模塊契約，模塊契約包含三個部分：使用假設條件(assume?condition)定義模塊執行的前提條件;使用保證條件(guarantee?condition)定義模塊執行的期望條件；如果靜態模塊的執行過程插入動態模塊，使用依賴條件(rely?condition)約束動態模塊的執行過程；

步驟3.使用程序證明方法驗證靜態模塊M是否滿足其模塊契約(假設條件assume、保證條件guarantee、依賴條件rely)，驗證靜態模塊M相對于其模型契約滿足正確性具體如下：

3-1.使用程序證明方法驗證靜態模塊M執行前的程序狀態滿足模塊的假設條件assume，如果滿足繼續執行步驟3-2，如果不滿足則靜態模塊M不滿足其模塊契約，返回步驟2；

3-2.?使用程序證明方法驗證靜態模塊M的執行過程滿足模塊的依賴條件rely,如果滿足繼續執行步驟3-3，如果不滿足則靜態模塊M不滿足其模塊契約，返回步驟2；

3-3.?使用程序證明方法驗證靜態模塊M執行后的程序狀態確保模塊的保證條件guarantee,如果滿足則靜態模塊M滿足其正確性約束，如果不滿足則靜態模塊M不滿足其模塊契約，返回步驟2；

步驟4.根據靜態模塊M的模塊契約，在動態模塊D中插入運行時檢查代碼：一部分檢查代碼負責檢查模塊M的的假設條件assume在依賴條件rely下是否是穩定的，另一部分檢查代碼負責檢查模塊M的保證條件assume在依賴條件下rely是否是穩定的，然后執行步驟5；

步驟5.運行JavaScript程序的模塊，如果執行過程插入動態模塊，執行相應的運行時檢查代碼，如果正確則是正確的模塊組合，如果不正確則是錯誤的模塊組合。

本發明的有益效果如下：

本發明通過分離動態語法特性，將JavaScript劃分為靜態模塊和動態模塊，靜態模塊增量組合動態模塊；使用信賴-保證方法定義JavaScript程序模塊的模塊約束，能夠確保JavaScript程序模塊在動態語法特性的影響下依然穩定，支持JavaScript程序模塊的增量組合。

附圖說明

圖1為本發明使用程序證明方法驗證靜態模塊是否滿足其模塊契約的流程圖。

圖2為本發明使用信賴-保證方法增量組合JavaScript程序的流程圖。

具體實施方式

下面結合附圖對本發明作進一步說明。

如圖1、圖2所示，一種增量組合JavaScript程序模塊的方法，具體包括如下步驟：