SHF: Small: Collaborative Research: Specification Language Foundations for Modular Reasoning Methodologies

SHF：小型：协作研究：模块化推理方法的规范语言基础

• 批准号: 0916715
• 负责人: Gary Leavens
• 金额: $ 25万
• 依托单位: The University of Central Florida Board of Trustees
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-08-01 至 2015-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0916715&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Specification

This project extends the semantical foundations of object-oriented (OO) languages to cover methodologies for modular reasoning. Modular reasoning means verifying software components assuming the specification of each used component. Modularity is important for productivity and scalability, but is difficult to achieve for OO software. To support modular reasoning, researchers have proposed several methodologies that restrict programs and their specifications. The goal of this project is to provide a theoretical basis that supports practical techniques for justifying and using methodologies.This project provides guidance for the designers of programming and specification languages, verification logics, and associated tools. The results will improve the utility and extensibility of verification tools --- a key goal of the Verified Software grand challenge. Software developers may benefit from the integration and harmonious interoperation of best-practice methodologies. This project is potentially transformative: it aims to enable combinations and customizations of methodologies by tool users, scalable to real applications.Improved OO programming methodologies may greatly improve programming practice, especially in applications needing high assurance, reliability, and security. This will benefit society, which increasingly depends on computing systems built using OO components. Unification of methodologies and streamlining of tools also facilitates the education of software developers.

这个项目扩展了面向对象（OO）语言的语义基础，以涵盖模块化推理的方法。模块化推理意味着假设每个使用的组件的规范来验证软件组件。模块化对于生产力和可伸缩性很重要，但对于OO软件来说很难实现。为了支持模块化推理，研究人员提出了几种限制程序及其规范的方法。该项目的目标是提供一个理论基础，支持证明和使用方法的实用技术。该项目为编程和规范语言，验证逻辑和相关工具的设计者提供指导。结果将提高验证工具的实用性和可扩展性-验证软件大挑战的一个关键目标。 软件开发人员可以从最佳实践方法的集成和和谐的互操作中受益。这个项目是潜在的变革：它的目的是使组合和定制的方法的工具用户，可扩展到真实的application.Improved面向对象编程方法可能会大大提高编程实践，特别是在应用程序需要高保证，可靠性和安全性。 这将使社会受益，因为社会越来越依赖于使用OO组件构建的计算系统。方法的统一和工具的精简也促进了软件开发人员的教育。