Specifications for modular program verifiers are expressed as constraints on program states (e.g. preconditions) and relations on program states (e.g. postconditions). For programs whose domain is managing resources of any kind (e.g. cryptocurrencies), such state-based specifications must make explicit properties that a human would implicitly understand for free. For example, it's clear that depositing into your bank account will not change other balances, but classically this must be stated as a frame condition. As a result, specifications for resource-manipulating programs quickly become verbose and difficult to interpret, write and debug. In this paper, we present a novel methodology that introduces user-defined first-class resources in the specification language, allowing resource-related operations and properties to be expressed directly and eliminating the need to reify implicit knowledge in the specifications. We implement our methodology as an extension of the program verifier Prusti, and use it to verify a key part of a real-world blockchain application. As we demonstrate in our evaluation, specifications written with our methodology are more concise, syntactically simpler, and easier to understand than alternative specifications written purely in terms of program states.

翻译：用于模块化程序验证器的规格说明通常表示为对程序状态的约束（如前置条件）和程序状态间的关系（如后置条件）。对于以管理各类资源（例如加密货币）为领域的程序而言，这种基于状态的规格说明必须显式化那些人类可凭直觉理解却无需言明的属性。例如，向银行账户存款显然不会改变其他账户余额，但传统方法必须将其表述为框架条件。这导致资源操作程序的规格说明迅速变得冗长，难以解读、编写和调试。本文提出了一种新颖的方法论，在规格说明语言中引入用户定义的一等资源，使得资源相关操作和属性能够被直接表达，从而消除规格说明中隐含知识的具体化需求。我们将该方法实现为程序验证器Prusti的扩展，并将其用于验证现实世界区块链应用的关键部分。实验评估表明，与纯粹基于程序状态编写的传统规格说明相比，采用本方法编写的规格说明更加简洁、语法更简单且更易理解。