Formal Methods for Multimethod Software Components

9803843本项目研究面向对象(OO)软件组件编程的形式化方法。目标是产生：(A)支持对此类组件进行仔细推理的理论基础，以及(B)能够替代此类组件源代码的可表达的行为接口规范语言(BISL)。目标(A)的基本问题包括具有可变对象的抽象数据类型的模型理论和证明理论、子类型、别名和消息传递。我们以前工作的模型理论被扩展到解释非确定性和高阶过程。在证明论中，人们寻求对不变对象进行推理的等式推理技术。这些结果将与具有多方法新特性的面向对象语言的验证逻辑联系在一起。目标(B)帮助供应商向客户解释OO类库和框架，而不向他们提供源代码，这是现有BISL无法完成的。该项目提供：设计更具表现力的OO规范语言的指导，在OO类库和框架的文档中使用的思想，以及规范的表现力符号。软件工程师还将受益于更具表现力的BISL和推理思想。*

9803843 This project investigates formal methods for programming object- oriented (OO) software components. The goals are to produce: (a) theoretical foundations to support careful reasoning about such components, and (b) expressive behavioral interface specification languages (BISLs) that are able to substitute for the source code of such components. Foundational issues for goal (a) include the model theory and proof theory of abstract data types with mutable objects, subtyping, aliasing, and message passing. The model theory of our previous work is extended to account for nondeterminism and higher-order procedures. In proof theory, equational reasoning techniques for reasoning about immutable objects are sought. These results are to be connected with verification logics for OO languages with the new feature of multimethods. Goal (b) helps vendors explain OO class libraries and frameworks to customers without giving them source code, which cannot be done with existing BISLs. This project provides: guidance for the design of more expressive OO specification languages, ideas for use in documentation of OO class libraries and frameworks, and expressive notations for specification. Software engineers will also benefit from more expressive BISLs and the ideas about reasoning.***