在Erlang中使用合约进行验证
Runtime verification in Erlang by using contracts
摘要：
在其生命周期中，程序会经历几次更改，这些更改旨在改进或增强其功能的某些部分。但是，这些修改通常也会引入影响已经工作的代码的错误。有几种方法和工具可以帮助发现和找到这些错误的来源。然而，这些错误中的大多数都可以通过使用程序员在编写代码时所掌握的一些知识来预先避免。这是契约式设计方法背后的思想，用户可以定义在运行时可以检查的契约。在本文中，我们将这种方法的原则应用于Erlang，以这种方式，在这种语言中实现运行时验证系统。我们定义了两种类型的合同。其中一种类型可以在任何Erlang程序中使用，而第二种类型仅用于并发程序。我们提供了这两种类型的合同的实施细节。此外，我们还提供了每个合同的详细解释以及它们的使用示例。本文提出的所有思想已在一个基于契约的运行时验证系统EDBC中实现。它的源代码可以在GitHub上作为开源和免费项目获得。
英文摘要：
During its lifetime, a program suffers several changes that seek to improve or to augment some parts of its functionality. However, these modifications usually also introduce errors that affect the already-working code. There are several approaches and tools that help to spot and find the source of these errors. However, most of these errors could be avoided beforehand by using some of the knowledge that the programmers had when they were writing the code. This is the idea behind the design-by-contract approach, where users can define contracts that can be checked during runtime. In this paper, we apply the principles of this approach to Erlang, enabling, in this way, a runtime verification system in this language. We define two types of contracts. One of them can be used in any Erlang program, while the second type is intended to be used only in concurrent programs. We provide the details of the implementation of both types of contracts. Moreover, we provide an extensive explanation of each contract as well as examples of their usage. All the ideas presented in this paper have been implemented in a contract-based runtime verification system named EDBC. Its source code is available at GitHub as an open-source and free project.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
