摘要：运用行为子类型及扩充行为子类型的概念,通过对一个Java实例地剖析,讨论了在面向 对象的契约式程序设计中如何撰写契约,以保持面向对象的单个继承和多重继承的特性问题,并证明 了这一方法的有效性。最后探讨了动态环境下违反契约时的责任归咎,展望了契约思想在软件开发 中的运用前景。

摘要：采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这个调用的前置条件,根据这些条件形式化求解调用的最强后置条件,也就是调用的语义作用。

摘要：介绍了契约式设计的思想,并在业务构件的分析中引入了契约式设计,从而构造出可信的业务构件。重点分析了契约式设计如何通过前置条件、后置条件和不变式3要素保证业务构件的可信,并给出具体的实例来说明。

摘要：实现了一个C#语言的合约检查工具,用于辅助程序员在用C#语言编写软件的时候运用合约式设计方法。工具将书写在程序注释中的合约提取出来,并转化为类不变式、类方法的前置条件或后置条件的检查代码插入到源文件中。当执行含有合约检查代码的源文件的时候,检查代码将被执行,以确保合约是否被遵守。

摘要：重构可以改进软件设计、提高软件质量。自动化重构工具的使用可以避免手工重构时引入的错误,提高软件开发效率。UML自动重构能充分利用UML特性,增加重构过程的直观性,并对重构在软件结构层次的实施提供了保障。本文结合重构技术的研究和UML技术的发展,给出了基于基本重构的分层,在此基础上分析了重构中行为维持问题的解决,提出了一个 UML模型自动重构的框架和详细设计实现,分析了它工作原理和各主要组件的功能。

摘要：提出一种支持程序开发的结构化方法．该方法以一种简单的问题分解策略为基础，比Ｗｉｒｔｈ－Ｄｉｊｋｓｔｒａ的自顶向下逐步求精方法更利于面向目标的程序设计．由该方法可知，一个程序可经一系列求精而开发出来，每一步求精都能为相应的最弱前置条件序列建立后置条件．这种策略使情况分析减少到极限，简化了结构化程序的证明，并保证了程序结构和数据结构之间的对应．