docs/Kernel-Operational-Semantics.md
[!IMPORTANT] This page was copied from https://github.com/dart-lang/sdk/wiki and needs review. Please contribute changes to bring it up-to-date - removing this header - or send a CL to delete the file.
The small-step operational semantics of Dart Kernel is given by an abstract machine in the style of the CEK machine. The machine is defined by a single step transition function where each step of the machine starts in a configuration and deterministically gives a next configuration. There are several different configurations defined below.
x ranges over variables, ρ ranges over environments, K ranges over expression continuations, A ranges over application continuations, E ranges over expressions, S ranges over statements, V ranges over values.
Environments are finite functions from variables to values. ρ[x → V] denotes the environment that maps x to V and y to ρ(y) for all y ≠ x.
An expression configuration indicates the evaluation of an expression with respect to an environment and an expression continuation.
| Expression configuration | Next configuration |
|---|---|
| <x, ρ, K><sub>expr</sub> | <K, ρ(x), ρ><sub>cont</sub> |
| <x = E, ρ, K><sub>expr</sub> | <E, ρ, VarSetK(x, K)><sub>expr</sub> |
| <!E, ρ, K><sub>expr</sub> | <E, ρ, NotK(K)><sub>expr</sub> |
| <E<sub>1</sub> and E<sub>2</sub>, ρ, K><sub>expr</sub> | <E<sub>1</sub>, ρ, AndK(E<sub>2</sub>, K)><sub>expr</sub> |
| <E<sub>1</sub> or E<sub>2</sub>, ρ, K><sub>expr</sub> | <E<sub>1</sub>, ρ, OrK(E<sub>2</sub>, K)><sub>expr</sub> |
| <E<sub>1</sub>? E<sub>2</sub> : E<sub>3</sub>, ρ, K><sub>expr</sub> | <E<sub>1</sub>, ρ, ConditionalK(E<sub>2</sub>, E<sub>3</sub>, K)><sub>expr</sub> |
| <StringConcat(exprList), ρ, K><sub>expr</sub> | <exprList, ρ, StringConcatenationA(K)><sub>exprList</sub> |
| <print(E), ρ, K><sub>expr</sub> | <E, ρ, PrintK</sub>(K)><sub>expr</sub> |
| <f(exprList), ρ, K><sub>expr</sub> | <exprList, ρ, StaticInvocationA(S : f.body, K)><sub>exprList</sub> |
| <BasicLiteral, ρ, K><sub>expr</sub> | <K, BasicLiteral, ρ><sub>cont</sub> |
| <Let x = E<sub>1</sub> in E<sub>2</sub>, ρ, K><sub>expr</sub> | <E<sub>1</sub>, ρ, LetK(x, E<sub>2</sub>, ρ, K)><sub>expr</sub> |
An expression continuation configuration indicates the application of an expression continuation K to a value and an environment. The environment is threaded to the continuation because expressions can mutate the environment.
| Expression continuation configuration | Next configuration |
|---|---|
| <VarSetK(x, K), V, ρ><sub>cont</sub> | <K, V, ρ[x → V]><sub>cont</sub> |
| <PrintK(K), V, ρ><sub>cont</sub> | <K, ∅, ρ><sub>cont</sub> |
| <ExpressionListK(exprList, A), V, ρ><sub>cont</sub> | <exprList, ρ, ValueApplicationA(V, A)><sub>exprList</sub> |
| <ExpressionK(C), V, ρ ><sub>cont</sub> | C |
An expression list configuration indicates the evaluation of a list of expressions with respect to an environment and an application continuation.
| Expression list configuration | Next configuration |
|---|---|
| <∅, ρ, A><sub>exprList</sub> | <A, ∅><sub>acont</sub> |
| <E :: tail, ρ, A><sub>exprList</sub> | <E, ρ, ExpressionListK(tail, A)><sub>expr</sub> |
An application continuation configuration indicates the application of A to a list of values.
| Application continuation configuration | Next configuration |
|---|---|
| <StaticInvocationA(S, K), valList><sub>acont</sub> | <S, ρ[formalList → valList], ∅, ExitC(K), K><sub>exec</sub> |
| <ValueApplicationA(V, A), valList><sub>acont</sub> | <A, V :: valList><sub>acont</sub> |
A statement configuration indicates the execution of a statement with respect to an environment.
S ranges over statements, L ranges over labels, C ranges over statement configurations.
| Statement configuration | Next configuration |
|---|---|
| <Expression(E), ρ, L, C, K><sub>exec</sub> | <E, ρ, ExpressionK(C)><sub>expr</sub> |