Effectful Software Contracts
Effectful Software Contracts
复制标题
DOI：
10.1145/3632930
复制
发表时间：
2024-01-01
影响因子：
1.8
通讯作者：
Felleisen，Matthias
中科院分区：
文献类型：
--
作者：
Moy，Cameron;Dimoulas，Christos;Felleisen，Matthias
软件契约使程序员能够描述组件的功能属性。然而，当涉及到约束效应时，文献只为各种效应提供了一次性的解决方案。它缺乏一个普遍的原则。本文提出了一个有效的合同系统的设计，在效果处理程序的背景下。一个关键的元定理表明，合同不能不适当地干扰程序的执行。该设计的实现，沿着其通用性的评价，表明该理论可以指导实践。
Software contracts empower programmers to describe functional properties of components. When it comes to constraining effects, though, the literature offers only one-off solutions for various effects. It lacks a universal principle. This paper presents the design of an effectful contract system in the context of effect handlers. A key metatheorem shows that contracts cannot unduly interfere with a program's execution. An implementation of this design, along with an evaluation of its generality, demonstrates that the theory can guide practice.