We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker.

翻译：我们继续开发TinySol——一种基于Solidity（以太坊平台标准智能合约语言）的极简面向对象语言。首先，我们为TinySol扩展了异常处理机制和Gas计量机制，并为其配备了小步操作语义。引入Gas计量机制对于在TinySol中模拟现实智能合约至关重要，因为这是确保以太坊智能合约正常终止的常规方式。随后，我们设计了一套针对智能合约的类型系统，保证此类程序在运行时永远不会耗尽Gas。这对智能合约而言是理想特性，因为耗尽Gas的交易会被中止，但执行代码所支付的费用不会返还给调用者。