关键词:
MSVL
时序逻辑
Python
解释器
程序设计语言
摘要:
软硬件系统的正确性和可靠性十分重要,一个微小的漏洞在某些系统中可能造成重大的财产和安全损失。除了软件测试方法外,形式化验证方法也是提高软硬件系统正确性和可靠性的重要途径。时序逻辑常被用于形式化验证,并且得到了广泛应用。MSVL(Modeling,Simulation and Verification Language)来源于投影时序逻辑(Projection Temporal Logic,PTL),是实验室自主研发的程序设计语言,具有建模、仿真和验证功能,可以提高软硬件系统的正确性和可靠性。Python是一种功能强大的解释型程序设计语言,具有灵活性、交互性和可扩展性等特点。Python语言语法简单,易学易用,是其受到广泛使用的原因之一。相较之下,MSVL缺乏交互性,并且语法较为复杂。但是Python存在运行效率低、缺乏可靠性的问题,灵活的动态类型容易导致运行时错误。除此之外,活跃的开源社区虽然提供了大量功能强大的开源库,但同时也引入了潜在的漏洞。本文主要研究了一个类Python程序设计语言XD-M的设计与实现,主要贡献如下:***-M语言设计的重点是其解释器的设计。设计了 XD-M语言解释器的整体框架,选用易于在Windows和Linux双端进行移植的开发环境。设计了 XD-M语言的词法和语法,词法和语法规则主导着XD-M语言的编程风格。以MSVL为基础参照了 Python语句,实现了类似于Python的一种使用简单变量而不涉及类型声明的编程风格,围绕着赋值、结构体、内置函数和基本语句的词法和语法设计进行了详细地介绍。2.解决了 XD-M语言解释器底层实现的关键问题,对各种形式的赋值、结构体定义、内置函数和外部导入语句等关键问题,使用语法树的形式进行了直观描述,并对解决方案进行了详细说明。3.以XD-M语言分别编写了求解四阶幻方和构建平衡二叉树的程序实例,对程序进行了仿真、建模和验证,说明了 XD-M语言及其解释器的可用性与实用性。