对象演算II

章应用Ｇｏｇｕｅｎ等人的结论证明并得到了几个结构化对象演算的基本定理。一方面,这些定理保证了该可由现有对象的描述构造新对象的描述,并且可以把建立在现有对象上的定理作为整个对象描述和验证的引理。另一方面,章还讨论了基于封装性的对象精化。于是得到一个结构化的对象演算系统。     

对象演算Ⅰ

对象演算是一个面向对象的逻辑演算系统,它建立在描述具有内部状态的动态演变实体的Trace演算之上.对象比一般意义下的动态实体具有更多和更好的特性,特别是封装性.为此,文章引入有效动作的概念,通过对象的有效动作来刻画对象的封装性,即只有对象的有效动作才能访问或修改对象的属性值,从而对Trace演算的语义模型加以限制,得到对象语义解释模型.作为逻辑系统,文章还讨论了对象演算的公理化,它是Trace演算公理系统的扩充.作为应用,文章结合实例给出了对象语义的描述及特性推理.     

对象演算I

对象演算是一个面向对象的逻辑演算系统,它建立在描述具有内部状态的动态演变实体的Ｔｒａｃｅ演算之上。对象比一般意义下的动态实体具有更多和更好的特性,特别是封装性。为此,章引入有效动作的概念,通过对象的有效动作来刻画对象的封装性,即只有对象的有效动作才能访问或修改对象的属性值,从而对Ｔｒａｃｅ演算的语义模型加以限制,得到对象语义解释模型。作为逻辑系统,章还讨论了对象演算的公理化,它是Ｔｒａｃｅ演算     

基于rCOS的UML状态图语义研究

统一建模语言（UML）中的状态图用于描述类的对象所有可能的状态及事件发生时状态的转移条件,从而进行系统动态分析。针对现有关于UML状态图形式化语义研究中存在的不足,该文提出基于统一程序设计理论的对象精化演算系统,用于描述UML状态图的形式化语义,给出与类图、序列图的一致性检验,为模型驱动开发提供了可行性。     

对象描述语言及其指称描述

在面向对象的软件构造中，对象被视为软件系统的基本构件．本文提出对象规范描述语言ＯＤＬ（ｏｂｊｅｃｔｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ），并给出其主要结构的ＳＯＰ指称描述．ＳＯＰ演算的理论范集给出对象的形式描述．ＳＯＰ理论范集反映了对象的封装性，在这样的逻辑框架下，对象的属性（结构）和动作（行为）得以统一．对象聚合提供了由已有对象描述构造复杂对象描述的机制；而继承则可以扩充给定的对象描述并保持原描述的特性．此外，本文还区分了继承和子类这２个相似而又不尽相同的概念.     

基于Atom的远程对象交换机制的研究

随着互联网的发展,Web2.0和Mash-up逐渐成为Web环境中的主要应用形式.针对现有远程对象交换机制的局限性,本文以Atom文档格式与Atom发布协议为基础建立了一种更易被Web2.0和Mash-up应用的远程对象交换机制.在兼顾半结构化数据与强类型语言结构化要求的条件下,利用Atom文档格式解决了远程对象的封装问题;利用Atom发布协议解决了远程对象的操作问题.在此基础上,通过性能评估和综合比较,说明该机制具有实现简单、适应半结构化数据、在少量易变数据时性能好等优点.     

对象工程──结构化方法和信息工程的继承和发展

对象工程是最新的、最优秀的、未定型的软件开发技术。文章详细比较了它与结构化方法、信息工程法的异同,并指出对象工程是结构化方法和信息工程的继承和发展。     

面向路桥施工问题求解的功能图形数据模型

针对现有路桥施工问题求解所常采用的工程数据模型的缺陷,提出了功能图形数据模型.以功能图形对象建模技术为指导,以特征线、特征线数组为基本数据结构描述具有可变长非结构化的工程图形,进行相关几何和专业计算,表达特征线数组间存在的协同合作关系,支持功能图形对象的动态计算过程,实现了一种利用简单数据结构创建复杂工程图形对象的新途...     

对象式Lambda演算的自作用部分计值

讨论了一个对象式Lambda演算的部分计值器.对象式Lambda演算在Lambda演算的基础上添加了对象机制.部分计值器的构造是采用传统的三步法,首先定义对象式Lambda演算的元解释器;然后提出对象式Lambda演算的约束时间分析方法(binding-timeanalysis),约束时间分析决定哪些计算可以在编译时完成,哪些计算需留在运行时执行;最后定义部分计值器,同时,给出了元解释器和部分计值器的正确性证明.     

描述逻辑μALCQO 的语义及推理

循环术语集是描述逻辑长期以来的研究难点,其最基本的问题即语义及推理问题没有得到合理的解决.基于混合分级μ-演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCQO 中,提出了一种允许包含循环术语集的描述逻辑μALCQO.给出了μALCQO 的语法、语义和不动点构造算子的性质,证明了μALCQO 的可满足性推理等价于混合分级μ-演算的可满足性推理.基于混合分级μ-演算可满足性推理算法,并利用完全强化自动机给出了μALCQO的可满足性推理算法,以及给出了推理算法正确性证明和复杂性定理.μALCQO为进一步给出同时含有不动点构造算子和枚举构造算子的表达能力强的描述逻辑推理算法提供了理论基础.     

面向对象类型理论的比较研究

人们已提出各种支持面向对象程序设计的类型理论。但每种类型理论的侧重点不足相同，它们均能解决面向对象程序设计的某些方面的问题。本文从对象、类、类型和继承角度，着重分析讨论抽象数据类型、记录演算和对象演算，为进一步研究关于面向对象程序设计的类型理论提供基础。     

Inferring additional knowledge from QTCN relations

It is widely held that people tend to use qualitative rather than quantitative phrases when raising or answering questions about moving objects. Queries about whether an object is moving towards or away from another object or whether objects are getting closer to each other or further away from each other, require qualitative responses. This characteristic should be reflected in a calculus to be used to describe and reason about continuously moving objects. In this paper, we present a qualitative trajectory calculus of relations between two disjoint moving objects, whose movement is constrained by a network. The proposed calculus (QTC_N) is formally introduced and illustrated. Particular attention is placed on how to infer additional knowledge from QTC_N relations by means of composition tables and the transformation of QTC_N relations into relations defined by the Relative Trajectory Calculus on Networks (RTC_N).     

基于扩展角色访问控制的普适计算访问控制模型

针对普适计算访问控制对客体部分动态管理的需要,分析了现有扩展基于角色的访问控制（RBAC）的不足,提出一种新的扩展RBAC模型。模型引入客体与客体的关联,使得权限既可以通过角色也可以通过客体获得,并采用描述逻辑对模型访问控制过程进行了形式化描述。该模型能够实现细粒度的动态授权,解决了因决策的固有性导致角色数量过多、授权不灵活的问题。     

A Rewriting Calculus for Cyclic Higher-order Term Graphs

Introduced at the end of the nineties, the Rewriting Calculus (ρ-calculus, for short) is a simple calculus that fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the obtained structured results are first class objects of the calculus. The evaluation mechanism, generalizing beta-reduction, strongly relies on term matching in various theories.In this paper we propose an extension of the ρ-calculus, handling graph like structures rather than simple terms. The transformations are performed by explicit application of rewrite rules as first class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.The calculus over terms is naturally generalized by using unification constraints in addition to the standard ρ-calculus matching constraints. This therefore provides us with the basics for a natural extension of an explicit substitution calculus to term graphs. Several examples illustrating the introduced concepts are given.