资源操纵程序的资源规格
摘要：资源模块化程序验证器的规范是通过对程序状态（例如前置条件）和程序状态关系（例如后置条件）的约束来表达的。对于管理任何类型资源（例如加密货币）的程序，这些基于状态的规范必须明确表达人类可以隐式理解的属性。例如，很明显，将钱存入银行账户不会改变其他余额，但传统上必须将其作为一个帧条件陈述。因此，资源操作性程序的规范很快变得冗长且难以解释、编写和调试。 在本文中，我们提出了一种新颖的方法，引入了用户定义的一流资源，使得资源相关的操作和属性可以直接表达，消除了在规范中体现隐含知识的需要。我们将这种方法作为程序验证器Prusti的扩展来实现，并将其用于验证实际区块链应用的关键部分。正如我们在评估中展示的那样，使用我们的方法编写的规范更为简洁、语法更简单，也更容易理解，而不是纯粹基于程序状态的备选规范。
作者：Zachary Grannan and Alexander J. Summers
论文ID：2304.12530
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-26