SHF: Small: Effectful Software Contracts

SHF：小型：有效的软件合同

• 批准号: 1117635
• 负责人: Amal Ahmed
• 金额: $ 44.08万
• 依托单位: Indiana University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-08-01 至 2011-11-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1117635&HistoricalAwards=false
• 关键词: SHF; Small; Effectful; Software; Contracts

The long-term goals of this project are to bring the technology ofsoftware contracts to widely-used programming languages and, throughthe use of manifest contracts, to provide software developers with amigration path from simply typed code to fully functional correctness.Since computational effects are notoriously hard to reason about andpervade even the simplest realistic programs, the proposed researchshould have significant impact on programmers' ability to developsoftware that is more reliable and more secure. Contracts in software establish clear interfaces between programcomponents. Like contracts in the legal realm, they delineate eachparty's expectations and obligations. Such contracts are becomingincreasingly important for the regulation of modern software systems,providing an expressive framework for verification and error tracking.To be effective in a software environment, contracts must have formalsemantics and must be supported by a monitoring system that preciselytracks the flow of values as they cross interfaces. To date, however,the formal study of contracts has mostly been limited to smallidealized languages without computational effects, such as readingdata from or writing data to a display or file, managing resourcessuch as memory, and performing probabilistic or speculativecomputation.This research aims to extend the semantic framework of softwarecontracts to languages with various computational effects: theextension is qualitative in nature and will enable the use ofcontracts in new application domains. Specifically, the PIs proposeto add support for computational effects to the two flavors ofcontracts studied to date: latent contracts, which are runtime checksnot reflected in the type system, and manifest contracts, where asystem of precise types records the most recent runtime check appliedto each value. The extension of latent contracts will be done in thecontext of a monadic met language. The extension of manifestcontracts will make use of a variant of Hoare Type Theory to preciselyrecord computational effects. The PIs will also implement prototypesystems and use them to present novel applications of softwarecontracts.

该项目的长期目标是将软件契约技术引入到广泛使用的编程语言中，并通过使用清单契约，为软件开发人员提供从简单类型代码到完全功能正确性的迁移路径。由于计算效果是出了名的难以推理，甚至在最简单的现实程序中也普遍存在，建议的研究应该对程序员开发更可靠和更安全的软件的能力产生重大影响。软件中的契约在程序组件之间建立了清晰的接口. 就像法律的领域的合同一样，它们描述了每一方的期望和义务。 这种契约对于现代软件系统的监管越来越重要，它为验证和错误跟踪提供了一个表达框架。为了在软件环境中有效，契约必须具有形式语义，并且必须得到一个监控系统的支持，该系统可以精确地跟踪跨接口的值流。 然而，到目前为止，对契约的正式研究大多局限于没有计算效应的小型理想化语言，例如从显示器或文件读取数据或向其写入数据，管理资源（如内存），以及执行概率或推测计算。本研究旨在将软件契约的语义框架扩展到具有各种计算效应的语言：该扩展是定性的，并将使合同的使用在新的应用领域。 具体来说，PI建议为迄今为止研究的两种类型的契约增加对计算效果的支持：潜在契约，这是类型系统中没有反映的运行时检查，以及清单契约，其中精确类型的系统记录应用于每个值的最新运行时检查。 潜在契约的扩展将在一元语言的上下文中完成。 显式契约的扩展将利用霍尔类型理论的一个变体来精确地记录计算效果。 PI还将实现原型系统，并使用它们来展示软件合同的新应用。