MSVL: a typed language for temporal logic programming. 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 extendMSVL 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 theMSV toolkit with the support of modeling, simulation and verification of typedMSVL programs. Applications to the construction of AVL tree and ordered list show the practicality of the language.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Shu, Xinfeng; Duan, Zhenhua; Du, Hongwei: A decision procedure and complete axiomatization for projection temporal logic (2020)
- Shu, Xinfeng; Zhang, Nan; Wang, Xiaobing; Zhao, Liang: Efficient decision procedure for propositional projection temporal logic (2020)
- Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang: Translating Xd-C programs to MSVL programs (2020)
- Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei: A novel approach to verifying context free properties of programs (2020)
- Zhao, Liang; Wang, Xiaobing; Shu, Xinfeng; Zhang, Nan: A sound and complete proof system for a unified temporal logic (2020)
- Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)