基于类型理论的面向对象多步证明系统

介绍基于扩展构造型演算的交互式多步证明系统。该系统中以函数式语言ＭＬ为开发环境，建立了ＥＣＣ的项、规则证明策略和证明管理机制的描述，并引入规约类型、类类型、类和对象的表示，为面向对象的程序规约和定理证明系统的结合进行了一些探索。     

基于类型理论的面向对象程序设计

构造性类型理论可作为程序开发的理论基础，其中类型作为程序规约，证明过程作为程序开发过程，从证明抽取满足程序规约的程序．本文提出了一种构造性类型理论ＴＴＯＯＰ，引入了类规约类型和类类型的概念．类是类规约类型的元素，它又是一种类型，类的元素为对象．通过证明类规约可构造类，由此构造面向对象软件．     

基于类型理论面向对象程序设计

本文提出了一种构造性类型理论ＴＴＯＯＰ，引入了类现规类型和类类型的概念。类是类规约类型的元素，它又是一类型，类的元素为对象。通过证明类可构造类，由此构造面向对象软件。     

基于Tableau方法的程序综合系统——DTPS

本文简单介绍了基于Ｔａｂｌｅａｕ方法的程序综合系统－ＤＴＰＳ．ＤＴＰＳ系统以定理证明为基础，为构造一个满足程序规约的程序，只需证明的确存在一个满足条件的对象。如果这个证明存在，那么从证明中可抽取出一个满足该程序规约的程序。     

基于类型理论的继承机制的研究

本文提出了基于构造性类型理论的一种面向对象类型理论中的继承机制,认为类是类规约类型的元素,而且类也是一种类型,继承是类规约和程序开发过程的重用机制.本文提出的理论可用于面向对象程序自动化的研究.     

基于软件工程的规约方法分类

本文从软件工程角度,对软件的规约方法进行了分类。得到两类规约方法:一类是基于逻辑规约方法.此方法一般是给出系统应该满足的性质集合。其代表是时序逻辑方法。另一类方法是基于模型规约方法。此方法一般是给出一个抽象模型,这个抽象模型指出程序应该如何活动.其代表是通信系统演算(CCS).本文进一步从软件工程原理,对这两类规约方法进行了比较和讨论。得到的结论是:两种类型的规约方法在系统开发的整个过程中都起着不同而重要的作用,它们相辅相成,缺一不可.最后,指出了今后的研究工作.在软件开发中,应该考虑多种规约方法和多种语义相结全的开发过程.     

基于软件工程的规约方法分类

本文从软件工程角度,对软件的规约方法进行了分类,得到两类规约方法:一类是基于逻辑规约方法,此方法一般是给出系统应该满足的性质集合,其代表是时序逻辑方法;另一类方法是基于模型规约方法,此方法一般是给出一个抽象模型,这个抽象模型指出程序应该如何活动,其代表是通信系统演算(CCS)。本文进一步从软件工程原理,对这两类规约方法进行了比较和讨论,得到的结论是:两种类型的规约方法在系统开发的整个过程中都起着不同而重要的作用,它们相辅相成,缺一不可.最后,我们指出了今后的研究工作.在软件开发中,应该考虑多种规约方法和多种语义相结合的开发过程.     

基于设计演算的形式化用例分析建模框架

提出一种形式化用例分析建模框架,引入类图、用例顺序图、用例状态图、功能规约函数和系统不变式从多个角度为需求建模.通过定义这些视图的形式化语义,为需求的各个方面定义了准确的形式化描述.利用该框架,可以从方法的交互行为规约和功能规约合成描述方法全部行为的全规约;也可以定义用例模型的性质,并通过设计演算中的证明来分析验证这些性质.作为应用,研究了检查用例模型一致性的规则.给出一个实例说明建模框架的可行性.     

SMV的观察迁移系统的模型检测分析

模型检验技术是开发高可信系统的重要途径.提出了一种基于定理证明的模型验证方法,并实现了工具验证.它以代数规约语言CafeOBJ描述系统的无限状态并把它转换成有限状态的SMV规约.通过观察迁移系统,证明产生的SMV规约的反例即CafeOBJ规约的反例,来找出开发早期阶段的系统的潜在错误,从而避免时间、金钱的耗费及重复性的劳动.     

一种程序综合方法

通过证明程序规约的方法可构造相应程序，但对“难题”和无证明的规约，无法使用这种方法构造程序，另一方面，如果可构造程序规约的验证程序，则可把这种程序看成该仙约的程序。本文讨论了程序规约的验证程序的构造方法，作为研究程序自动佛的一种途径。     

XYZ/E面向对象程序语义概述

XYZ/E面向对象程序中表示对象概念的语言成分是代理机构:一种由一个数据包块和与之匹配的进程所组成的模块.在时序逻辑框架下给出了面向对象程序及其包含的各种语言成分的语义,并提供了几个用于证明这些语言成分之间的语义一致性的定理.     

基于PROBE方法的DWFC内聚度量改进

利用有向带权伪图（Directed Weighted False Chart, DWFC）表示面向对象程序中类内部成员间的依赖关系，提出一种基于DWFE的面向对象类内聚度量方法，结合PSP（Personal Software Process）技术中PROBE（PROx Based Estimating）规模估算方法，改进了良好内聚度量方法的验证准则，并结合实验验证了该方法的优越性。     

Object-oriented programming with class dictionaries

A class dictionary defines all data structures that appear in a program as well as a language for describing data specified by the data structures. We demonstrate that class dictionaries are ideal for simplifying object-oriented programming. Our class dictionary-based approach to object-oriented programming is independent of any particular programming language, so it is applicable to a large variety of object-oriented systems. The experience in designing and using over one hundred class dictionaries has resulted in a set of useful design techniques. This novel approach to object-oriented programming makes interesting links between language design, data structure design, and data-base design.     

Modeling and visualizing object-oriented programs with Codecharts

Software design, development and evolution commonly require programmers to model design decisions, visualize implemented programs, and detect conflicts between design and implementation. However, common design notations rarely reconcile theoretical concerns for rigor and minimality with the practical concerns for abstraction, scalability and automated verifiability. The language of Codecharts was designed to overcome these challenges by narrowing its scope to visual specifications that articulate automatically-verifiable statements about the structure and organization of object-oriented programs. The tokens in its visual vocabulary stand for the building-blocks of object-oriented design, such as inheritance class hierarchies, sets of dynamically-bound methods, and their correlations. The formalism was tailored for those pragmatic concerns which arise from modeling class libraries and design patterns, and for visualizing programs of any size at any level of abstraction. We describe design verification, a process of proving or refuting that a Java program (i.e. its native code) conforms to the Codechart specifying it. We also describe a toolkit which supports modeling and visualization with Codecharts, as well as a fully-automated design verification tool. We conclude with empirical results which suggest gains in both speed and accuracy when using Codecharts in software design, development and evolution.     

An executable object-oriented semantics and its application to firewall verification

This paper presents a formal executable semantics of object-oriented models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing it within the expressive intersection of the functional programming language ML and the theorem prover HOL. In this paper, we present the definition and implementation of the semantics. We also present a prototype verification tool ObjectLogic which supports simulation and theorem proving on the semantics. As a case study, we show the verification of a practical firewall system.     

面向对象软件类测试研究新进展

软件测试是软件开发过程中不可缺少的一环,是保证软件质量和提高软件可靠性的关键.近年来,随着面向对象软件开发方法应用的更加广泛和研究的不断深入,面向对象软件测试已成为软件工程领域的一个重要研究课题.类是面向对象软件的基本构成单元,类测试是面向对象软件测试的关键.从基于状态、基于规范、基于UML、基于方法序列、基于数据流等6方面论述了类测试的目前研究成果,分析了研究现状,探讨了进一步工作的方向.     

基于VC+ +的航天器姿态控制系统设计与仿真

针对采用结构化方法设计航天器仿真软件效率低的问题,基于VC 采用面向对象思想提出了一种航天器姿态动力学与控制的仿真框架。设计了一种航天器的姿态控制器,并给出了系统稳定性证明;在理论上证明了控制律的全局渐近稳定后,在所设计出的VC 仿真软件上验证了控制算法。所提出的航天器仿真软件设计方法成功应用于某型航天器姿态控制系统,实现了仿真软件的可重用性,提高了软件的可扩充性,优化了代码,取得了明显的效果。     

Automatic Generation of UML Class Diagrams for Object-oriented Design and Programing Course

UML Class diagram generation from textual requirements is an important task in object-oriented design and programing course. This study proposes a method for automatically generating class diagrams from Chinese textual requirements on the basis of Natural Language Processing (NLP) and mapping rules for sentence pattern matching. First, classes are identified through entity recognition rules and candidate class pruning rules using NLP from requirements. Second, class attributes and relationships between classes are extracted using mapping rules for sentence pattern matching on the basis of NLP. Third, we developed an assistant tool integrated into a precision micro classroom system for automatic generation of class diagram, to effectively assist the teaching of object-oriented design and programing course. Results are evaluated with precision, accuracy and recall from eight requirements of object-oriented design and programing course using truth values created by teachers. Our research should benefit beginners of object-oriented design and programing course, who may be students or software developers. It helps them to create correct domain models represented in the UML class diagram.     

面向对象产品装配模型的研究

对产品装配表达要求、产品设计过程要求进行了深入的探讨，基于产品装配对象的分析，提出了一个面向对象的产品装配模型。设计和实现了装配模型类及类层次结构，对该模型在产品信息的表达和管理，面向对象特性，支持Top-Down设计等方面进行了讨论和分析。该装配模型在软件系统设计中得到了很好的应用。     

An interface between object-oriented databases and relational databases

Currently relational databases are widely used, while object-oriented databases are emerging as a new generation of database technology. This paper presents a methodology to provide effective sharing of information in object-oriented databases and relational databases. The object-oriented data model is selected as a common data model to build an integrated view of the diverse databases. An object-oriented query language is used as a standard query language. A method is developed to transform a relational data definition to an equivalent object-oriented data definition and to integrate local data definitions. Two distributed query processing methods are derived. One is for general queries and the other for a special class of restricted queries. Using the methods developed, it is possible to access distributed object-oriented databases and relational databases such that the locations and the structural differences of the databases are transparent to users.