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

Study of Picto-Object Based on Algebraic-Temporal Logic

本文首先讨论了国内外有关面向对象方法学、代数规范、时态逻辑的研究现状 ,分析了对象形式化语义研究的不足 .其次 ,分析了几种主要的系统形式化模型和方法 .然后 ,在我们已研究的“计算机甲骨文象形码输入法”的基础上 ,从时态逻辑的角度定义了象形对象及其约束条件 ,定义了面向对象的有色 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.