SHF: Small: Effectful Software Contracts

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

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.