Formal Methods for Extensible Object-Oriented Software

可扩展的面向对象软件的形式化方法

• 批准号: 0097907
• 负责人: Gary Leavens
• 金额: $ 20万
• 依托单位: Iowa State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-06-01 至 2004-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0097907&HistoricalAwards=false
• 关键词: Formal; Methods; Extensible; Object; Oriented

This project advances the theory and practice of extensible object-oriented (OO) software by investigating how to support careful design, specification, and reasoning. Enhancing theoretical understanding for specifying and verifying extensible OO software forms the first subproblem. The project investigates several avenues: the soundness of proof techniques for behavioral subtyping among abstract data types with mutable objects, whose operations may have nondeterministic specifications; the extent to which the use of multimethods affects one's ability to prove behavioral subtyping; and the soundness of a specification and verification technique that allows the implementation of a subclass from a superclass's specification, without seeing the superclass's code.The second subproblem comprises enhancing Java and a specification language for Java to better support extensible OO frameworks and libraries. The project implements and refines MultiJava, an extension to Java that supports both open classes and multimethods. The former allow one to extend existing classes with new methods, while the latter allow one to easily extend both a set of data types and the methods that work on them. The project also extends and refines JML, which is a behavioral interface specification language tailored to Java.

该项目通过研究如何支持仔细的设计、规范和推理，推进了可扩展的面向对象（OO）软件的理论和实践。加强对指定和验证可扩展OO软件的理论理解形成了第一个子问题。该项目研究了几个途径：具有可变对象的抽象数据类型（其操作可能具有不确定性规范）的行为子类型的证明技术的可靠性；使用多种方法对一个人证明行为亚型的能力的影响程度；规范和验证技术的健全性，允许从超类的规范实现子类，而无需查看超类的代码。第二个子问题包括增强Java和Java规范语言，以更好地支持可扩展的OO框架和库。该项目实现并改进了MultiJava，这是Java的一个扩展，支持开放类和多方法。前者允许使用新方法扩展现有的类，而后者允许轻松地扩展一组数据类型和处理它们的方法。该项目还扩展和改进了JML，这是一种为Java量身定制的行为接口规范语言。