带事件的 Solidity 合约的形式化规约与验证
编程语言
2020-05-22 v1 计算机科学中的逻辑
软件工程
摘要
Solidity 语言中的事件提供了去中心化应用的链上服务与其用户之间的通信手段。事件通常被用作从用户视角相关的合约执行的抽象。因此, 用户必须能够理解所发出事件的含义并信任其有效性。本文提出一种源级方法, 用于带事件 Solidity 合约的形式化规约与验证, 主要关注事件。我们的方法允许依据事件所追踪的链上数据, 以及定义区块链状态与事件所提供的抽象视图之间对应关系的谓词来规约事件。该方法在 Solidity 的模块化验证器 solc-verify 中实现, 并通过多个示例展示其适用性。
引用
@article{arxiv.2005.10382,
title = {Formal Specification and Verification of Solidity Contracts with Events},
author = {Ákos Hajdu and Dejan Jovanović and Gabriela Ciocarlie},
journal= {arXiv preprint arXiv:2005.10382},
year = {2020}
}