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图通过提供清晰易懂的规范，促进了正确可靠智能合约的开发与分析。