基于代数-时态逻辑的象形对象研究  

Study of Picto-Object Based on Algebraic-Temporal Logic

作　　者：胡金柱[1] 舒忠梅[2] 

机构地区：[1]华中师范大学计算机科学系,湖北武汉430079 [2]中山大学计算机科学系,广东广州510275

出　　处：《小型微型计算机系统》2002年第6期726-730,共5页Journal of Chinese Computer Systems

基　　金：湖北省自然科学基金资助研究项目

摘　　要：本文首先讨论了国内外有关面向对象方法学、代数规范、时态逻辑的研究现状 ,分析了对象形式化语义研究的不足 .其次 ,分析了几种主要的系统形式化模型和方法 .然后 ,在我们已研究的“计算机甲骨文象形码输入法”的基础上 ,从时态逻辑的角度定义了象形对象及其约束条件 ,定义了面向对象的有色 Petri网 (OOPEN) ,并应用 OOPEN描述了象形对象的层次结构 .最后 ,我们将代数规范与时态逻辑相结合 ,对象形对象的语义基础进行了一些研究 .In this paper,we first described the late research situation of Object Oriented methodology and Algebraic specification and Temporal Logical in domestic and abroad, which shows the lack of the object formal semantics. Secondly,the main formal models and methods of system are analysed.Thirdly,based on 'Computer Jia Gu Wen Picto Code input system' which we have developed,Picto Object and its constaints are defined from the aspect of Temporal Logic.Then,the definition of Object Oriented Color Petri Net(OOCPN) is given furthemore,the hierachical architecture of the Picto Object is depicted in OOCPN. Finally,we combines Algebraic specification with Temporal Logical to do some research on the semantic basic of the Picto Object.

关 键 词：代数-时态逻辑 象形对象 面向对象方法学 代数规范 时态逻辑 逻辑程序设计 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]