Operational Semantics of Supported Solidity Statements Sample Clauses

Operational Semantics of Supported Solidity Statements. ‌ We build on the small-step operational semantics for Solidity defined in [26], which enables us to reason about one computational step at a time. We have extended the semantics of [26] to support exceptions and return values. · ∈ ∈ { } We present the semantics of each supported Solidity statement as one or more rules. Each rule takes an execution state σ, an execution status N, E, R[v] , and a statement Stmt S, and maps them to a new execution state, a new exe- cution status, and a statement that remains to be executed (or if no statements are left to be executed). We start with basic rules that apply to every statement. If an exception has been raised or if a return statement has been executed, then no further statements should be executed, which is captured by the SKIP-EXC and SKIP- RET rules: SKIP-EXC ((σ, E), Stmt) → ((σ, E), ·) SKIP-RET ((σ, R[v]), Stmt) → ((σ, R[v]), ·) · A return statement changes the execution status to R[ ], skipping all re- maining statements, which is captured by the RETURN rule: RETURN ((σ, N ), return;) → ((σ, R[·]), ·) To return a value v, a return Exp statement changes the execution status to R[v], which is captured by the RETURN-VAL rule: RETURN-VAL Eval(σ, Exp) → ((σj, N ), v) ((σ, N ), return Exp;) → ((σj, R[v]), ·) If an exception is raised during the evaluation of Eval(σ, Exp), then execution status is changed to E, which is captured by the RETURN-EXC rule: RETURN-EXC Eval(σ, Exp) → ((σj, E), v) ((σ, N ), return Exp;) → ((σj, E), ·) { } A compound statement (i.e., a list of statements enclosed in braces and ) is executed by executing inner statements one after another, which is captured by the COMPOUND rule: ((σ, N ), Stmt1) → ((σ1, x1), ·) ((σ1, x1), Stmt2) → ((σ2, x2), ·)