[!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>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 |

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 |

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 |

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 |

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 |