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

無(wú)效

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

1.?一種增量組合JavaScript程序模塊的方法，其特征在于包括如下步驟：

步驟1.將JavaScript程序模塊分為靜態(tài)模塊M和動(dòng)態(tài)模塊D：靜態(tài)模塊M不包含動(dòng)態(tài)語(yǔ)法特性，支持程序靜態(tài)分析；動(dòng)態(tài)模塊D包含動(dòng)態(tài)語(yǔ)法特性，必須在運(yùn)行時(shí)進(jìn)行檢查；

步驟2.使用信賴-保證方法定義靜態(tài)模塊M的模塊契約，模塊契約包含三個(gè)部分：使用假設(shè)條件定義模塊執(zhí)行的前提條件;使用保證條件定義模塊執(zhí)行的期望條件；如果靜態(tài)模塊的執(zhí)行過(guò)程插入動(dòng)態(tài)模塊，使用依賴條件約束動(dòng)態(tài)模塊的執(zhí)行過(guò)程；

步驟3.使用程序證明方法驗(yàn)證靜態(tài)模塊M是否滿足其模塊契約，驗(yàn)證靜態(tài)模塊M相對(duì)于其模型契約滿足正確性；所述的模塊契約包括：假設(shè)條件、保證條件和依賴條件；

步驟4.根據(jù)靜態(tài)模塊M的模塊契約，在動(dòng)態(tài)模塊D中插入運(yùn)行時(shí)檢查代碼：一部分檢查代碼負(fù)責(zé)檢查靜態(tài)模塊M的假設(shè)條件在依賴條件下是否是穩(wěn)定的，另一部分檢查代碼負(fù)責(zé)檢查靜態(tài)模塊M的保證條件在依賴條件下是否是穩(wěn)定的，然后執(zhí)行步驟5；

步驟5.運(yùn)行JavaScript程序的模塊，如果執(zhí)行過(guò)程插入動(dòng)態(tài)模塊，執(zhí)行相應(yīng)的運(yùn)行時(shí)檢查代碼，如果正確則是正確的模塊組合，如果不正確則是錯(cuò)誤的模塊組合。

2.如權(quán)利要求1所述的一種增量組合JavaScript程序模塊的方法，其特征在于驗(yàn)證靜態(tài)模塊M相對(duì)于其模型契約滿足正確性具體如下：

3-1.使用程序證明方法驗(yàn)證靜態(tài)模塊M執(zhí)行前的程序狀態(tài)滿足模塊的假設(shè)條件，如果滿足繼續(xù)執(zhí)行步驟3-2，如果不滿足則靜態(tài)模塊M不滿足其模塊契約，返回步驟2；

3-2.?使用程序證明方法驗(yàn)證靜態(tài)模塊M的執(zhí)行過(guò)程滿足模塊的依賴條件,如果滿足繼續(xù)執(zhí)行步驟3-3，如果不滿足則靜態(tài)模塊M不滿足其模塊契約，返回步驟2；

3-3.?使用程序證明方法驗(yàn)證靜態(tài)模塊M執(zhí)行后的程序狀態(tài)確保模塊的保證條件,如果滿足則靜態(tài)模塊M滿足其正確性約束，如果不滿足則靜態(tài)模塊M不滿足其模塊契約，返回步驟2。