一种多类型MSVL语言解释系统及多类型MSVL语言解释方法

摘要

一种多类型MSVL语言解释系统其包括，变量类型声明模块、变量存储模块、算术表达式处理模块、赋值操作处理模块、强制类型转换命令处理模块及框架命令处理模块。在投影时序逻辑中及其程序设计语言MSVL中扩展了多种内置数据类型，增强了MSVL的描述能力，拓展了MSVL的应用领域，使MSVL可以更加灵活广泛地对多数据类型的系统进行建模和验证。本发明将变量的论域定义为取值和类型组成的二元组，将变量和常量的解释定义为二元组，使得每一个变量的类型作为变量的固有性质，提高变量引用的效率。针对于变量和常量的论域以及解释的扩展，给出相关函数和操作符的语义，使扩展类型后与类型相关的函数和运算符与现有的MSVL语句相兼容。

主权项

一种多类型MSVL语言解释系统，其特征在于，其包括，变量类型声明模块，其设置有变量类型声明命令以及类型声明定义，所述变量类型声明命令以MSVL变量声明语句的形式规定了变量的类型，MSVL包括了int，float，char以及string四种变量声明语句，扩展类型后MSVL中变量和常量的论域定义为DOMAIN，DOMAIN中的元素被定义为二元组，二元组的第一个分量表示变量的取值，而第二个分量标记了变量的类型，扩展类型后MSVL包括整型，浮点型以及字符型内置数据类型；变量存储模块，其设置有变量类型标记和变量取值，所述变量类型标记根据变量声明语句记录该变量的类型，变量的取值限制在其类型所对应的论域内；算术表达式处理模块，其用于多种类型的数据构造的算术表达式进行运算，其设置有：加法、减法、乘法、除法和取模运算的定义和处理模块，定义模块规定了各项算术运算的定义域和值域，算术运算的处理模块对操作数属于定义域的表达式进行解释，返回结果为相应值域中的一个常量；赋值操作处理模块，其对赋值操作进行处理，赋值操作符的左操作数是变量，右操作数是算术表达式，调用算术表达式处理模块对右操作数进行解释，然后将运算结果赋给变量；强制类型转换命令处理模块，其对算术表达式进行强制类型转换，强制类型转换命令以MSVL强制类型转换语句的形式修改变量的解释结果的类型和取值；以及，框架命令处理模块，其控制变量在未赋值的情况下，自动继承上一状态的取值。