框架时序逻辑语言MSVL中面向对象机制的实现

doi:10.3969/j.issn.1001-2400.2010.03.031

J4 ›› 2010, Vol. 37 ›› Issue (3): 559-564+575.doi: 10.3969/j.issn.1001-2400.2010.03.031

框架时序逻辑语言MSVL中面向对象机制的实现

王小兵^1,2,3;段振华¹

(1. 西安电子科技大学计算理论与技术研究所，陕西西安 710071;
2. 西安电子科技大学综合业务网理论及关键技术国家重点实验室，陕西西安 710071;
3. 武汉大学软件工程国家重点实验室，湖北武汉 430072)

收稿日期:2009-11-10 出版日期:2010-06-20 发布日期:2010-07-23
作者简介:王小兵(1979-)，男，讲师，博士，E-mail: xbwang@foxmail.com．
基金资助:
国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金重大国际合作资助项目(60910004);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);陕西省科技攻关计划资助项目(2009K01-36);中央高校基本科研业务费专项资金资助项目(JY10000903004,JY10000903014)

Implementation of objected-oriented mechanism in framed temporal logic language MSVL

WANG Xiao-bing^1,2,3;DUAN Zhen-hua¹

(1. Research Inst. of Computing Theory, Xidian Univ., Xi'an 710071， China;
2. Technology and State Key Lab. of Integrated Service Networks, Xidian Univ., Xi'an 710071， China;
3. State Key Lab. of Software Eng., Wuhan Univ., Wuhan 430072， China)

Received:2009-11-10 Online:2010-06-20 Published:2010-07-23

摘要/Abstract

摘要：

针对目前时序逻辑语言存在框架问题、缺少面向对象机制、形式化程度过高等不足，提出了框架时序逻辑语言MSVL，包含新的框架操作符、等待语句和非确定的选择语句等技术，并且能够支持面向对象的程序设计．基于正则形和正则图，给出了MSVL解释器的实现方案．并发访问共享资源的实例表明，MSVL比其他时序逻辑语言更接近高级语言，并且解释器的实现方案是切实可行的．

关键词: 框架, 时序逻辑, 时序逻辑语言, 面向对象程序设计, 解释器

Abstract:

In order to overcome the shortages which the available temporal logic programming languages have such as existence of the frame problem, lack of object-oriented mechanisms and high formalization, the framed temporal logic language MSVL is defined, which includes some techniques such as new frame operator, await statement, nondeterministic choice statement,and object-oriented programming. The implementation plan for the interpreter for MSVL is proposed based on the normal form and normal form graph. An example for concurrent access to shared resources shows that MSVL is much more similar to high-level programming languages than other temporal logic languages, and that the implementation plan for the interpreter is workable.

Key words: framing, temporal logic, temporal logic language, object oriented programming, interpreter

王小兵;段振华. 框架时序逻辑语言MSVL中面向对象机制的实现[J]. J4, 2010, 37(3): 559-564+575.

WANG Xiao-bing;DUAN Zhen-hua. Implementation of objected-oriented mechanism in framed temporal logic language MSVL[J]. J4, 2010, 37(3): 559-564+575.

参考文献

[1]Miao Huaikou, Zeng Hongwei. Model Checking-based Verification of Web Application[C]//The Proceeding of ICECCS 2007. Auckland: IEEE Computer Society Press, 2007: 47-55.
[2]Moszkowski B C. Executing Temporal Logic Programs[M]. Cambridge: Cambridge University Press, 1986.
[3]Lamport L. The Temporal Logic of Actions[J]. ACM Trans on Programming Languages and Systems, 1994, 16(3): 872-923.
[4]Duan Z, Koutny M. A Framed Temporal Logic Programming Language[J]. Journal of Computer Science and Technology, 2004, 19(3): 341-351.
[5]唐稚松. 时序逻辑程序设计与软件工程[M]. 北京: 科学出版社, 1999.
[6]Duan Z, Yang X, Koutny M. Framed Temporal Logic Programming[J]. Science of Computer Programming, 2008, 70(1): 31-61.
[7]王小兵, 段振华. 框架投影时序逻辑程序设计语言中的指针[J]. 西安电子科技大学学报, 2008, 35(6): 1069-1074.
Wang Xiaobing, Duan Zhenhua. Pointers in Framing Projection Temporal Logic Programming Languages[J]. Journal of Xidian University, 2008, 35(6): 1069-1074.
[8]Mccarthy J, Hayes P J. Some Philosophical Problems from the Standpoint of Artificial Intelligence[M]. Edinburgh: Machine Intelligence 4, Edinburgh University Press, 1969.
[9]Ma Y, Duan Z, Wang X, et al. An Interpreter for Framed Tempura and Its Application[C]//The Proceeding of TASE 2007. Shanghai: IEEE Press, 2007: 251-260.
[10]王小兵, 段振华. 面向对象的时序逻辑语言[J]. 电子科技大学学报, 2009, 38(1): 97-101.
Wang Xiaobing, Duan Zhenhua. Object-Oriented Temporal Logic Language[J]. Journal of University of Electronic Science and Technology of China, 2009, 38(1): 97-101.
[11]Duan Z. Temporal Logic and Temporal Logic Programming[M]. Beijing: Science Press, 2006.
[12]王小兵. 面向对象MSVL语言及其在组合Web服务验证中的应用[D]. 西安: 西安电子科技大学, 2009.
[13]Duan Z, Tian C. A Unified Model Checking Approach with Projection Temporal Logic[C]//The Proceeding of ICFEM 2008. Berlin: Springer-Verlag, 2008: 167-186.
[14]Levine J. Flex & Bison: Text Processing Tools[M]. 1st ed. Sebastopol: O'Reilly Media, 2009.

[1]	王禹博,孙蓉,刘景伟. 分布式存储中新型分组piggybacking框架[J]. 西安电子科技大学学报, 2023, 50(3): 132-141.
[2]	刘惠,董锡耀,杨志涵. 融合Stacking框架的BiGRU-LGB云负载预测模型[J]. 西安电子科技大学学报, 2023, 50(3): 83-94.
[3]	宁晓晗,雷维嘉. 能量收集多天线发送机的功率控制和天线选择[J]. 西安电子科技大学学报, 2022, 49(3): 83-92.
[4]	张璐,孙蓉,刘景伟. 分布式存储中的克隆piggybacking框架[J]. 西安电子科技大学学报, 2020, 47(6): 139-147.
[5]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[6]	赵辉,张乐,刘莹莉,张静,张天骐. 低相干高鲁棒性观测矩阵优化[J]. 西安电子科技大学学报, 2019, 46(6): 171-178.
[7]	马倩;段振华. MSVL程序的自动定理证明方法[J]. J4, 2016, 43(1): 75-81.
[8]	吴玉莲;冯象初. 利用平衡方法的非凸图像修复[J]. J4, 2014, 41(5): 141-147.
[9]	张紫楠;郭渊博;杨奎武;黄惠新;杨占海. 通用可组合认证密钥交换协议[J]. J4, 2014, 41(5): 185-191.
[10]	逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.
[11]	张南;段振华. 进位保留加法器的命题投影时序逻辑组合验证[J]. J4, 2012, 39(5): 192-196.
[12]	杨琛;段振华. 支持Stutter-不变性的命题区间时序逻辑[J]. J4, 2011, 38(2): 151-156.
[13]	杨潇潇;段振华. MSVL语言的公理系统的程序验证[J]. J4, 2010, 37(1): 96-101.
[14]	李青山;王梅圣;赵晨光;王英强. 面向系统集成领域的多Agent智能协作模型[J]. J4, 2010, 37(1): 62-67.
[15]	舒新峰;段振华. 投影时序逻辑的公理系统与形式验证[J]. J4, 2009, 36(4): 680-729.

框架时序逻辑语言MSVL中面向对象机制的实现

Implementation of objected-oriented mechanism in framed temporal logic language MSVL

PDF (PC)

赞

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0