Smart contracts manage blockchain assets. While smart contracts embody business processes, their platforms are not process-aware. Mainstream smart contract programming languages such as Solidity do not have explicit notions of roles, action dependencies, and time. Instead, these concepts are implemented in program code. This makes it very hard to design and analyze smart contracts. We argue that DCR graphs are a suitable formalization tool for smart contracts because they explicitly and visually capture these features. We utilize this expressiveness to show that many common high-level design patterns in smart-contract applications can be naturally modeled this way. Applying these patterns shows that DCR graphs facilitate the development and analysis of correct and reliable smart contracts by providing a clear and easy-to-understand specification.

翻译：智能合约管理区块链资产。虽然智能合约体现了业务流程，但其平台并不具备流程感知能力。主流智能合约编程语言（如 Solidity）缺乏对角色、动作依赖性和时间的显式定义，这些概念反而在程序代码中实现，导致智能合约的设计与分析极为困难。我们认为 DCR 图是适用于智能合约的形式化工具，因其能显式且可视化地捕获这些特性。我们借助其表达能力证明，智能合约应用中许多常见的高级设计模式均可通过此方式自然建模。应用这些模式表明，DCR 图通过提供清晰易懂的规范，促进了正确可靠的智能合约的研发与分析。