SHF: Small: Higher-order Contracts for Distributed Applications

SHF：小型：分布式应用程序的高阶合约

• 批准号: 1421770
• 负责人: Stephen Chong
• 金额: $ 45.64万
• 依托单位: Harvard University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-08-01 至 2017-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1421770&HistoricalAwards=false
• 关键词: SHF; Small; Higher; order; Contracts

Distributed applications (such as web applications and cloud-based applications, where multiple computers cooperate to run the application) are becoming increasingly common. Given the amount of commercial activity and information handled by these distributed applications, it is important that these applications are correct, reliable, and efficient. However, many traditional tools and techniques for programmers cannot be used for distributed applications, making it difficult for programmers to write and debug distributed applications. This research explores the use of software contracts for distributed applications. Software contracts are specifications for software components that can be checked at run time (i.e., when the software executes). By developing techniques and tools to incorporate software contracts into distributed applications, this research has the potential to make it easier for programmers to write distributed applications that are correct, reliable, and efficient.Specifically, this research explores the use of higher-order contracts for distributed applications. Higher-order contracts are contracts for higher-order values such as first-class functions or objects. Higher-order contracts are a good fit for distributed applications as components in distributed applications are often higher-order, and higher-order contracts facilitate reasoning about dynamic composition of components (which is common in distributed settings such as web applications). Potential benefits of higher-order contracts include: (a) declarative specification of the functional behavior of components; (b) run-time enforcement of specifications; and (c) correct identification of faulty components. This research focuses on the efficient enforcement of behavioral contracts, the correct enforcement of contracts in the presence of untrustworthy distributed components, and the specification and enforcement of non-functional behaviors.

分布式应用程序（如web应用程序和基于云的应用程序，其中多台计算机协作运行应用程序）正变得越来越普遍。考虑到这些分布式应用程序处理的商业活动和信息的数量，确保这些应用程序正确、可靠和高效是非常重要的。然而，许多面向程序员的传统工具和技术不能用于分布式应用程序，这使得程序员很难编写和调试分布式应用程序。本研究探讨了分布式应用程序中软件契约的使用。软件契约是软件组件的规范，可以在运行时（即软件执行时）进行检查。通过开发将软件契约合并到分布式应用程序中的技术和工具，这项研究有可能使程序员更容易编写正确、可靠和高效的分布式应用程序。具体来说，本研究探讨了分布式应用程序中高阶契约的使用。高阶契约是高阶值的契约，如第一级函数或对象。高阶契约非常适合分布式应用程序，因为分布式应用程序中的组件通常是高阶的，而高阶契约有助于对组件的动态组合进行推理（这在web应用程序等分布式设置中很常见）。高阶契约的潜在好处包括：(a)组件功能行为的声明性规范；(b)规范的运行时强制执行；(c)正确识别故障部件。本研究的重点是行为契约的有效执行，在不可信的分布式组件存在下契约的正确执行，以及非功能行为的规范和执行。