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.***