公开(公告)号：CN103150199B

公开(公告)日：2016-03-02

申请号：CN201310120181.7

申请日：2013-04-08

Applicant: 西安电子科技大学

Inventor： 段振华 ,  李洁 ,  王小兵 ,  田聪 ,  张南 ,  于研 ,  杨凯

IPC: G06F9/45 ,  G06F9/46

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

公开(公告)号：CN103150199A

公开(公告)日：2013-06-12

申请号：CN201310120181.7

申请日：2013-04-08

Applicant: 西安电子科技大学

Inventor： 段振华 ,  李洁 ,  王小兵 ,  田聪 ,  张南 ,  于研 ,  杨凯

IPC: G06F9/45 ,  G06F9/46

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