欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言．为了证明区间时序逻辑程序的正确性，提出了MSVL语言的一个公理系统：包括正则形转换的状态公理和状态推演规则，以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则．最后给出验证实例说明基于该公理系统的程序验证方法．
英文摘要：
The language MSVL is an interval temporal logic programming language. It can be used for the purpose of modeling, simulation and verification of programs. To prove the correctness of interval temporal logic programs, we present a proof system for MSVL. To do so, a set of state axioms and state inference rules is given to deduce a program into its normal form. In addition, a set of axioms and inference rules over intervals is formalized to transform a program from one state to another. Finally, an example is given to illustrate how the axiom system works.
同期刊论文项目
同项目期刊论文
位置：