MSVL： a typed language for temporal logic programming

作     者：Xiaobing WANG Cong TIAN Zhenhua DUAN Liang ZHAO 

作者机构：ICTT and ISN Lab Xidian University Xi'an 710071 China 

出 版 物：《Frontiers of Computer Science》 (中国计算机科学前沿（英文版）)

年 卷 期：2017年第11卷第5期

页      面：762-785页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金 the Fundamental Research Funds for the Central Universities 

主　　题：type temporal logic programming MSVL type declaration struct definition 

摘      要：The development of types is an important but challenging issue in temporal logic programming. In this paper, we investigate how to formalize and implement types in the temporal logic programming language MSVL, which is an executable subset of projection temporal logic （PTL）. Specifically, we extend MSVL with a few groups of types including basic data types, pointer types and struct types. On each type, we specify the domain of values and define some standard operations in terms of logic functions and predicates. Then, it is feasible to formalize statements of type declaration of program variables and statements of struct definitions as logic formulas. As the implementation of the theory, we extend the MSV toolkit with the support of modeling, simulation and verification of typed MSVL programs. Applications to the construction of AVL tree and ordered list show the practicality of the language.