Collaborative Research: Formal Methods for Behavioral Subclassing and Callbacks

协作研究：行为子类化和回调的形式化方法

• 批准号: 0429894
• 负责人: David Naumann
• 金额: --
• 依托单位: Stevens Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2004
• 资助国家: 美国
• 起止时间: 2004-09-01 至 2008-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0429894&HistoricalAwards=false
• 关键词: Collaborative; Research; Formal; Methods; Behavioral

Proposals 0429894/Naumann 0429567/LeavensCollaborative Research:Formal Methods for Behavioral Subclassing and CallbacksDavid A. Naumann and Gary T. LeavensFor evolvability, scalability, and productivity, software systems must be composed of extensible components. Features of object-oriented programming languages such as inheritance and dynamic dispatch, andtechniques like callbacks and downcalls, are crucial but they invert the usual layering of abstractions. Aliasing among objects is crucial for efficiency but can breach encapsulation boundaries. Yet abstractionand encapsulation are necessary to separately validate individual components.This project will advance the theory of specification, development, and verification for object-oriented software, focusing on behavioral subclassing, alias confinement, and callbacks. Core features of theJava Modeling Language (JML) for behavioral interface specification will be studied, using a confinement discipline to control aliasing and model programs to specify callbacks. The ideas will be presentedin a cogent, simple, and robust theory, to facilitate applications by tools, comparison between alternative proposals for specification notations and proof rules, and teaching. The theory will be encodedin a theorem prover and key results machine-checked.This project will provide theoretical guidance for the designers of programming and specification languages. The results will also help clarify and improve techniques used in practice.Direct application is expected in projects based on JML and in work by our Brazilian collaborators.

提案 0429894/Naumann 0429567/Leavens 协作研究：行为子类化和回调的形式方法David A. Naumann 和 Gary T. Leavens 为了实现可演化性、可扩展性和生产力，软件系统必须由可扩展组件组成。面向对象编程语言的特性（例如继承和动态分派）以及回调和向下调用等技术至关重要，但它们颠倒了通常的抽象分层。 对象之间的别名对于效率至关重要，但可能会破坏封装边界。 然而，抽象和封装对于单独验证各个组件是必要的。该项目将推进面向对象软件的规范、开发和验证理论，重点关注行为子类化、别名限制和回调。 将研究用于行为接口规范的 Java 建模语言 (JML) 的核心功能，使用限制规则来控制别名和模型程序来指定回调。 这些想法将以令人信服、简单且稳健的理论来呈现，以促进工具的应用、规范符号和证明规则的替代建议之间的比较以及教学。 该理论将被编码在定理证明器中，并对关键结果进行机器检查。该项目将为编程和规范语言的设计者提供理论指导。 结果还将有助于澄清和改进实践中使用的技术。预计将在基于 JML 的项目和我们巴西合作者的工作中直接应用。