Kernel Operational Semantics

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.

Expression configuration

An expression configuration indicates the evaluation of an expression with respect to an environment and an expression continuation.

Expression configuration	Next configuration
<x, ρ, K>expr	<K, ρ(x), ρ>cont
<x = E, ρ, K>expr	<E, ρ, VarSetK(x, K)>expr
<!E, ρ, K>expr	<E, ρ, NotK(K)>expr
<E1 and E2, ρ, K>expr	<E1, ρ, AndK(E2, K)>expr
<E1 or E2, ρ, K>expr	<E1, ρ, OrK(E2, K)>expr
<E1? E2 : E3, ρ, K>expr	<E1, ρ, ConditionalK(E2, E3, K)>expr
<StringConcat(exprList), ρ, K>expr	<exprList, ρ, StringConcatenationA(K)>exprList
<print(E), ρ, K>expr	<E, ρ, PrintK(K)>expr
<f(exprList), ρ, K>expr	<exprList, ρ, StaticInvocationA(S : f.body, K)>exprList
<BasicLiteral, ρ, K>expr	<K, BasicLiteral, ρ>cont
<Let x = E1 in E2, ρ, K>expr	<E1, ρ, LetK(x, E2, ρ, K)>expr

Expression continuation configuration

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, ρ>cont	<K, V, ρ[x → V]>cont
<PrintK(K), V, ρ>cont	<K, ∅, ρ>cont
<ExpressionListK(exprList, A), V, ρ>cont	<exprList, ρ, ValueApplicationA(V, A)>exprList
<ExpressionK(C), V, ρ >cont	C

Expression list configuration

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>exprList	<A, ∅>acont
<E :: tail, ρ, A>exprList	<E, ρ, ExpressionListK(tail, A)>expr

Application continuation configuration

An application continuation configuration indicates the application of A to a list of values.

Application continuation configuration	Next configuration
<StaticInvocationA(S, K), valList>acont	<S, ρ[formalList → valList], ∅, ExitC(K), K>exec
<ValueApplicationA(V, A), valList>acont	<A, V :: valList>acont

Statement configuration

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>exec	<E, ρ, ExpressionK(C)>expr