-
Notifications
You must be signed in to change notification settings - Fork 1.7k
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, 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>expr | <K, ρ(x), ρ>cont |
<x = E, ρ, K>expr | <E, ρ, VarSet(x, K)>expr |
<f(exprList), ρ, K>expr | <exprList, ρ, StaticInvocation(S : f.body, K)>exprList |
An expression continuation configuration indicates the application of an expression continuation to a value and an environment. The environment is threaded to the continuation because expressions can mutate the environment.
Expression continuation configuration | Next configuration |
---|---|
<VarSet(x, K), V, ρ>cont | <K, V, ρ[x → V]>cont |
<ExpressionList(tail, A), V, ρ>cont | <tail, ρ, ValueApplication(V, A)>exprList |
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, ∅>cont |
<E :: tail, ρ, A>exprList | <E, ρ, ExpressionList(tail, A)>expr |
An expression list continuation configuration indicates the application of an application continuation to a list of values.
Expression list continuation configuration | Next configuration |
---|---|
<StaticInvocation(S, K), valList>cont | <S, ρ[formalList → valList]>exec |
<ValueApplication(V, A), valList>cont | <A, V :: valList>cont |
Important
The wiki has moved to https://github.com/dart-lang/sdk/tree/main/docs; please don't edit the pages here.