基于代数-时态逻辑的象形对象语义模型探讨  

A Tentaitive Approach of Picto-Object Semantic's Model Based on Algebraic -Temporal Logic

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

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

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

基　　金：湖北省自然科学基金项目

摘　　要：本文在 "基于代数 -时态逻辑的象形对象研究 "一文的基础上 ,进一步讨论了“基于代数 -时态逻辑的象形对象语义模型”问题 .主要是将基于代数模型和基于时态逻辑模型这两种方法结合 ,通过 OOCPN描述形式 ,对象形对象语义模型进行了探索式研究 .具体包括象形对象标记、象形对象语义解释结构、象形对象语义结构模型结构 ,定义了状态运算符、操作运算符并给出其语义域上的解释 ;提出了可继承属性和可继承操作、完全继承和部分继承等概念 ,并用来刻画象形对象系统中的类结构及继承性 ;在分类结构、组装结构的基础上提出了聚合类结构及分类 -聚合类结构 ;给出了象形对象类类型的代数规范描述 ;给出了有关象形对象系统的公理和定理 ,并用 OOCPN(Object- Oriented ColorPetri Net)对象形对象的继承性、类结构及类变化、重码语义的可能性和有害性等进行了描述 .In this paper,we combines Algebraic specification with Temporal Logical to do some trial research on the semantic of the Picto Object by use of OOCPN(Object Oriented Color Petri Net),on the basis of 'Study of Picto Object Based on Algebraic Temporal Logic'. The semantic model of the Picto Object are described ;Picto Object semantics interpreting structure and Picto Object semantic model structure are given;the state opertor and the operate oprator as well as Picto trace are defined. Then, we proposes inheritable attribute,inheritable operate, full inheritances concepts and part inheritaces concepts and aggregation class structure and classified aggregation class structure for the Picto Object. In the meanwhile, we gives the algebraic specification of the Picto Objects class type. Based on these theories,we proposes some axioms about Picto Objects semantic model,and illustrates Picto Objects inheritance,Picto Objects class structure and multi code semantics characteristics in OOCPN.

关 键 词：代数-时态逻辑 象形对象 语义模型 代数规范 面向对象 形式语义 计算机 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]