[发明专利]一种混合验证JavaScript程序正确性的方法

摘要

本发明公开了一种混合验证JavaScript程序正确性的方法。本发明包括以下步骤：将JavaScript程序划分为静态部分和动态部分两大部分；使用开放时态逻辑规约JavaScript程序的正确性；使用程序证明方法验证静态部分正确性和静态动态部分组合的正确性；使用模型检测方法验证动态部分的正确性。本发明验证方法能够适应JavaScript语言的多种语法特性和应用场合，既能支持自动化的模型检测工具，又能有效的降低状态搜索空间，有效提高JavaScript程序的验证效率。

主权项

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.针对静态部分的程序规约，建立开放系统的有限状态机模型，其中静态部分抽象成开放系统的内部迁移，动态部分抽象成开放系统的外部迁移，外部迁移对开放系统的影响必须确保系统的正确性，并使用模型检测工具验证系统的正确性，如果验证正确则程序正确，如果发现错误则程序验证错误。