| % Copyright (c) 2017, the Dart project authors. Please see the AUTHORS file |
| % for details. All rights reserved. Use of this source code is governed by a |
| % BSD-style license that can be found in the LICENSE file. |
| |
| |
| \documentclass[a4paper,oneside,fleqn]{article} |
| |
| |
| \usepackage[utf8]{inputenc} |
| \usepackage[fleqn]{amsmath} |
| \usepackage{a4wide} |
| \usepackage{url} |
| \usepackage{cite} |
| \usepackage{amssymb} |
| \usepackage{stmaryrd} |
| \usepackage{alltt} |
| \usepackage{xypic} |
| \usepackage{appendix} |
| \usepackage{color} |
| \usepackage{hyperref} |
| \usepackage{chngcntr} |
| \usepackage{ifthen} |
| \usepackage[fleqn]{mathtools} |
| \usepackage{geometry} |
| \usepackage{mdframed} |
| \usepackage[textsize=tiny]{todonotes} |
| \usepackage{mathrsfs} |
| |
| \definecolor{shade}{gray}{0.75} |
| \newcommand{\shadethis}[1]{\colorbox{shade}% |
| {\protect\rule[-0.95mm]{0mm}{3.95mm}\hspace{0.3mm}#1\hspace{0.3mm}}} |
| |
| |
| % Shorthard for ``Dart Kernel'' in small caps. |
| \newcommand{\kernel}{\textsc{Dart Kernel}} |
| |
| % Shorthand for ``Dart'' in small caps. |
| \newcommand{\dart}{\textsc{Dart}} |
| |
| % A bit nicer symbol: ∅ |
| \renewcommand{\emptyset}{\varnothing} |
| |
| % Some known sets. |
| \newcommand{\NN}{\mathbb{N}} % Natural numbers. |
| |
| |
| % Some auxiliary operators. |
| \DeclareMathOperator{\dom}{Dom} % Domain of a function. |
| |
| |
| % Meta-functions to be used in math mode. |
| \DeclareMathOperator{\extend}{extend} |
| \DeclareMathOperator{\update}{update} |
| \DeclareMathOperator{\extendMain}{extendMain} |
| \DeclareMathOperator{\concat}{concat} |
| \DeclareMathOperator{\getter}{implicitGetter} |
| \DeclareMathOperator{\setter}{implicitSetter} |
| \DeclareMathOperator{\lookup}{lookup} |
| \DeclareMathOperator{\methodLookup}{methodLookup} |
| \DeclareMathOperator{\contains}{contains} |
| |
| % Meta-functions for operations on list |
| \DeclareMathOperator{\head}{head} |
| \DeclareMathOperator{\tail}{tail} |
| \DeclareMathOperator{\append}{append} |
| |
| % Keywords and syntactic constructs of Dart Kernel to be used in math mode. |
| \newcommand{\synt}[1]{\ensuremath{\text{\textbf{\texttt{#1}}}}} |
| \DeclareMathOperator{\dowhile}{\synt{do~while}} |
| \DeclareMathOperator{\while}{\synt{while}} |
| \DeclareMathOperator{\forin}{\synt{for~in}} |
| \DeclareMathOperator{\for}{\synt{for}} |
| \DeclareMathOperator{\throw}{\synt{throw}} |
| \DeclareMathOperator{\rethrow}{\synt{rethrow}} |
| \DeclareMathOperator{\new}{\synt{new}} |
| \DeclareMathOperator{\nnull}{\synt{null}} |
| \DeclareMathOperator{\bbreak}{\synt{break}} |
| \DeclareMathOperator{\switch}{\synt{switch}} |
| \DeclareMathOperator{\continue}{\synt{continue}} |
| \DeclareMathOperator{\return}{\synt{return}} |
| \DeclareMathOperator{\case}{\synt{case}} |
| \DeclareMathOperator{\default}{\synt{default}} |
| \DeclareMathOperator{\try}{\synt{try}} |
| \DeclareMathOperator{\catch}{\synt{catch}} |
| \DeclareMathOperator{\finally}{\synt{finally}} |
| |
| % Functions for projection on components of class. |
| \DeclareMathOperator{\superclass}{\synt{superclass}} |
| \DeclareMathOperator{\members}{\synt{members}} |
| \DeclareMathOperator{\lookupMember}{\synt{lookupMember}} |
| \DeclareMathOperator{\class}{\synt{class}} |
| \DeclareMathOperator{\getfield}{\synt{field}} |
| |
| |
| % Oftenly used syntactic meta-literals. |
| \newcommand{\true}{\synt{true}} |
| \newcommand{\false}{\synt{false}} |
| \newcommand{\this}{\synt{this}} |
| \newcommand{\Rethrow}{\synt{rethrow}} |
| \newcommand{\Throw}[1]{\synt{throw}\,#1} |
| |
| % Syntactic Domains |
| \newcommand{\dexpr}{\mathbf{Expr}} |
| \newcommand{\dstmt}{\mathbf{Stmt}} |
| \newcommand{\dhandler}{\mathbf{Handler}} |
| |
| \newcommand{\decont}{\mathbf{ExprCont}} |
| \newcommand{\dscont}{\mathbf{StmtCont}} |
| \newcommand{\dacont}{\mathbf{ApplCont}} |
| \newcommand{\dbcont}{\mathbf{BreakCont}} |
| \newcommand{\dswitchcont}{\mathbf{SwitchCont}} |
| \newcommand{\dncont}{\mathbf{EventCont}} |
| |
| \newcommand{\dlbl}{\mathbf{Label}} |
| \newcommand{\dclbl}{\mathbf{SwitchLabel}} |
| |
| \newcommand{\denv}{\mathbf{Env}} |
| \newcommand{\dmenv}{\mathbf{MainEnv}} |
| \newcommand{\dfield}{\mathbf{Field}} |
| |
| \newcommand{\dval}{\mathbf{Value}} |
| \newcommand{\dlit}{\mathbf{Literal}} |
| \newcommand{\dvar}{\mathbf{Variable}} |
| \newcommand{\dvardecl}{\mathbf{VariableDeclaration}} |
| \newcommand{\dstring}{\mathbf{StringValue}} |
| \newcommand{\dfunval}{\mathbf{FunctionValue}} |
| \newcommand{\dlitval}{\mathbf{LiteralValue}} |
| \newcommand{\dobjval}{\mathbf{ObjectValue}} |
| \newcommand{\dvector}{\mathbf{Vector}} |
| \newcommand{\dmember}{\mathbf{Member}} |
| \newcommand{\dident}{\mathbf{Identifier}} |
| \newcommand{\idmeta}{\ensuremath{\mathit{X}}} |
| \newcommand{\dtype}{\mathbf{Type}} |
| |
| \newcommand{\typemeta}{\ensuremath{\mathit{t}}} |
| \newcommand{\dclass}{\mathbf{Class}} |
| \newcommand{\dformals}{\mathbf{Formals}} |
| |
| \newcommand{\ddom}{\mathbf{Dom}} % Unspecified domain to use in examples. |
| |
| % Known domains for Dart types. |
| \newcommand{\dsemint}{\mathbf{int}} |
| \newcommand{\dsembool}{\mathbf{bool}} |
| \newcommand{\dsemdouble}{\mathbf{double}} |
| \newcommand{\dsemlist}{\mathbf{List}} |
| \newcommand{\dsemmap}{\mathbf{Map}} |
| \newcommand{\dsemstring}{\mathbf{String}} |
| \newcommand{\dsemsymbol}{\mathbf{Symbol}} |
| |
| |
| %% |
| % Commands to typeset transitions of CESK machine. |
| % |
| % \cesktrans{FROM}{TO} |
| % \cesktransalign{FROM}{TO} |
| % \cesktranssplit{FROM}{TO} |
| % |
| % Typesets a transition from configuration FROM to configuration TO. Like this: |
| % |
| % FROM => TO |
| % |
| % "Align" variant has an embedded "&" inside, immediately before the transition |
| % sign "=>". It means that the command should be put into an environment that |
| % aligns its multi-line content using "&" signs, for example "align". |
| % |
| % "Split" variant has an embedded "\\" inside, immediately after the transition |
| % sign "=>". It is useful for putting long equations in an environment such as |
| % "split". |
| %% |
| \newcommand{\cesktrans}[2]{\ensuremath{{#1} \Rightarrow {#2}}} |
| \newcommand{\cesktransalign}[2]{\ensuremath{{#1} &\Rightarrow {#2}}} |
| \newcommand{\cesktranssplit}[2]{\ensuremath{{#1} \Rightarrow\\ {#2}}} |
| |
| |
| %% |
| % Commands to typeset transitions of CESK machine with clarifying clause. |
| % |
| % \cesktranswhere{FROM}{TO}{WHERE} |
| % \cesktranswherealign{FROM}{TO}{WHERE} |
| % \cesktranswherealign*{FROM}{TO}{WHERE} |
| % \cesktranswheresplit{FROM}{TO}{WHERE} |
| % \cesktranswheresplit*{FROM}{TO}{WHERE} |
| % |
| % Typesets a transition from configuration FROM to configuration TO. These |
| % commands have a clarifying clause that explains the meaning of some new |
| % symbols introduced by the transition. |
| % |
| % The "align" versions have an embedded "&" inside, immideately before the |
| % transition sign "=>". It means that the command sould be put into an |
| % environment that aligns its multi-line content using "&" signs, for example |
| % "align". The non-starred "align" variant puts the additional clause to the |
| % same line as the transition itself, separating it with a comma. The starred |
| % version puts the additional clause on the next line. |
| % |
| % Here is how non-starred version looks like: |
| % |
| % FROM => TO, WHERE |
| % |
| % Here is how starred version looks like: |
| % |
| % FROM => TO, |
| % WHERE |
| % |
| % "Split" variants has embedded "\\" inside. Non-starred "split" variant have one |
| % after the comma. Starred "split" variant have one additional "\\" after |
| % the transition sign "=>". It is useful for putting long equations in an |
| % environment such as "split", "gather", or "multline". Note that if an |
| % environment generates a new equation number for each line, it can be disabled |
| % by putting "\notag" inside the arguments where the number is undesirable. |
| %% |
| \newcommand{\cesktranswhere}[3]{\ensuremath{{#1} \Rightarrow {#2}, {#3}}} |
| \newcommand{\cesktranswherealignNoStar}[3]{\ensuremath{{#1} &\Rightarrow {#2}, {#3}}} |
| \newcommand{\cesktranswherealignStar}[3]{\ensuremath{{#1} &\Rightarrow \begin{aligned}[t]&{#2},\\&{#3}\end{aligned}}} |
| \makeatletter |
| \newcommand{\cesktranswherealign}{% |
| \@ifstar |
| \cesktranswherealignStar% |
| \cesktranswherealignNoStar% |
| } |
| \makeatother |
| \newcommand{\cesktranswheresplitNoStar}[3]{\ensuremath{{#1} \Rightarrow {#2},\\{#3}}} |
| \newcommand{\cesktranswheresplitStar}[3]{\ensuremath{{#1} \Rightarrow\\ {#2},\\{#3}}} |
| \makeatletter |
| \newcommand{\cesktranswheresplit}{% |
| \@ifstar |
| \cesktranswheresplitStar% |
| \cesktranswheresplitNoStar% |
| } |
| \makeatother |
| |
| |
| \setlength{\itemsep}{0pt} |
| \geometry{% |
| top=2cm,% |
| right=2cm,% |
| bottom=2cm,% |
| left=3cm,% |
| } |
| |
| |
| \newmdenv[linecolor=black,leftline=false,rightline=false]{eqfigure} |
| |
| |
| \begin{document} |
| \title{Operational Semantics of \kernel{}} |
| \author{\kernel{} Team \\ \href{mailto:dart-kernel@google.com}{dart-kernel@google.com}} |
| |
| \maketitle |
| |
| \begin{abstract} |
| |
| The \kernel{} is a simplified representation of the \dart{} programming language. |
| Similar to the \textsc{Core} of the Glasgow Haskell Compiler, \kernel{} is more amenable to formal specification and analysis than the \dart{} surface language and is the primary intermediate representation used in the \dart{} compilation toolchain. |
| This paper documents the syntax and operational semantics of \kernel{} to enable framework authors for \dart{} to write safe transformations on \kernel{}, to allow the creation of a reference interpreter for testing the backend implementations of \dart{} and to facilitate academic analysis of the safety properties of \dart{}. |
| |
| \end{abstract} |
| |
| \setcounter{tocdepth}{2} |
| \tableofcontents |
| |
| \section{Foreword} |
| |
| \subsection{Audience} |
| This paper is intended for compiler and framework authors and academics. |
| The reader should have a proficient understanding of basic concepts in programming language design and implementation, such as abstract syntax, intermediate representations and operational semantics. |
| Still, this paper aims to be as accessible as possible, so most concepts that are not familiar to an advanced \dart{} programmer will be explained in sufficient detail to understand the formalizations here. |
| |
| \subsection{Formalization Style} |
| |
| \subsubsection{Abstract Syntax} |
| |
| The abstract syntax of \kernel{} is slightly unusual in that it does not have a tree structure or relate to any concrete, textual syntax. |
| It is instead a description of the data structures used by the \dart{} compliation toolchain, which are represented as directed acyclic graph. |
| The semantics depends heavily on the use of ``pointer'' equality between nodes in the syntax graph, which is more fine-grained than structural equality. |
| For example, a single \kernel{} program may have several syntax nodes that each define and initialize a variable with the same name and value, even in the same scope. |
| A later assignment to the variable will disambiguate between these declarations by referring to the specific variable declaration node by pointer identity. |
| Presenting the abstract syntax in this manner not only models the \kernel{} implementation more accurately, but allows us to ignore complications with variable renaming, shadowing and $\alpha$-conversion. |
| |
| \subsubsection{Small-step Operational Semantics} |
| |
| The operational semantics of \kernel{} are given in ``small-step'' style, where each rule of the semantics corresponds to a simple transition from one state of an abstract machine to another. |
| The rules are not nested or recursive, and only specify one possible outgoing transition from any state. |
| Some states of the machine have no outgoing transitions specified, corresponding to undefined operations like out-of-bounds vector access. |
| |
| \subsubsection{CESK Machine} |
| |
| The abstract machine is presented in the style of a CESK machine. \todo{dmitryas: add citation for CESK machine} |
| The state space of the CESK machine is grouped into several configurations, most of which carry an environment, which maps variable declarations in the present scope to their current assignments, a store, which models the mutable object store in which all objects in a \dart{} program live, and a continuation, which captures the work to be done after the current operation is complete, roughly similar to a chain of call frames above the current function. |
| In this way states of the CESK machine mimic states of the \dart{} virtual machine at a very abstract level. |
| |
| |
| \section{Definitions} |
| \label{sec:definitions} |
| |
| This section contains definitions of syntactic and semantic domains, helper functions, and notations used in the rest of the document. |
| |
| |
| \subsection{Conventions} |
| \label{subsec:conventions} |
| |
| \begin{itemize} |
| \item The symbols ``:'' (is-of-type) and ``$\in$'' (element-of) are used interchangeably. |
| \item The names of variables are italicized. |
| \item The names of variables within a syntactic domain start with an upper case letter. |
| \item The names of domains (meta-types defined in this paper) are written in bold (e.g. ``$\dexpr$''). |
| \item The names of the different kinds of continuations are written in normal text (e.g. VarSetEK). |
| \item The names of meta-functions start with lower case letter (e.g. $\extend$). |
| \item ``$\mlist{\ddom}$'' denotes the domain of meta-lists of elements from domain ``$\ddom$''. |
| Note that the word ``List'' here is not in bold, so that it isn't confused with the domain $\dsemlist$ of \dart{} objects. |
| \todo{sjindel: Why is this a domain?} |
| \end{itemize} |
| \todo{dmitryas: Explain notation for Kernel syntactic constructs like "on T catch (e, s)".} |
| |
| \subsection{Notations} |
| \label{subsec:notations} |
| |
| \begin{align*} |
| \dom(f) &\text{ --- the domain of function \(f\)}.\\ |
| \pi_i(x) &\text{ --- the $i^{th}$ component of $x \in \ddom_1 \times \dots \times \ddom_n$}. |
| \end{align*} |
| |
| \subsubsection{Meta list} |
| \label{subsubsec:meta-list} |
| |
| Throughout the document we use meta lists which represent lists of elements from some domain. |
| We define a list $l \in \mlist{\ddom}$ and are constructed as follows: |
| \begin{align*} |
| [] &\text{ --- empty list}.\\ |
| x :: \textit{list} &\text{ --- a meta-list that is constructed by adding element $x \in \ddom$ to the head of the meta-list $list$}. |
| \end{align*} |
| |
| \todo{Define behaviour for operations on empty list.} |
| In addition of the usual $\head$ and $\tail$ operations on a list, we add $\append$ operator. |
| \begin{align*} |
| &\head \in \mlist{\ddom} \rightarrow \ddom\\ |
| &\head(x :: \textit{list}) = x \text{ where $x :: \text{list} \in \mlist{\ddom}$}\\ |
| &\tail \in \mlist{\ddom} \rightarrow \mlist{\ddom}\\ |
| &\tail(x :: \textit{list}) = list \text{ where $x :: \text{list} \in \mlist{\ddom}$}\\ |
| &\append \in \mlist{\ddom} \times \ddom \rightarrow \mlist{\ddom}\\ |
| &\append(\textit{list}, x) = \textit{list'} \text{ where $x \in \ddom$ is the last element of $\textit{list}' \in \mlist{\ddom}$}\\ |
| \end{align*} |
| |
| |
| \subsection{Domains} |
| \label{subsec:domains} |
| |
| % Variables |
| \newcommand{\dlocation}{\mathbf{Location}} |
| \newcommand{\loc}{\ensuremath{\alpha}} |
| |
| \newcommand{\expr}{\ensuremath{\mathit{E}}} |
| \newcommand{\expri}[1]{\expr_\ensuremath{\mathit{#1}}} |
| \newcommand{\exprs}{\expr\ensuremath{\mathit{s}}} |
| \newcommand{\membermeta}{\ensuremath{\mathit{M}}} |
| |
| \newcommand{\stmt}{\ensuremath{\mathit{S}}} |
| \newcommand{\stmti}[1]{\stmt_\ensuremath{#1}} |
| \newcommand{\stmts}{\stmt\ensuremath{\mathit{s}}} |
| |
| \newcommand{\handler}{\ensuremath{\mathit{H}}} |
| \newcommand{\strace}{\ensuremath{\textit{st}}} |
| \newcommand{\cstrace}{\ensuremath{\textit{cst}}} |
| \newcommand{\cex}{\ensuremath{\textit{cex}}} |
| |
| \newcommand{\scase}{\mathit{SC}} |
| \newcommand{\scases}{\scase\ensuremath{\mathit{s}}} |
| \newcommand{\ccase}{\mathit{CC}} |
| \newcommand{\ccases}{\scase\ensuremath{\mathit{s}}} |
| |
| \newcommand{\vals}{\ensuremath{vs}} |
| \newcommand{\vvec}{\ensuremath{\vec{v}}} |
| |
| \newcommand{\env}{\ensuremath{\rho}} |
| \newcommand{\mainenv}{\env_{M}} |
| \newcommand{\field}{\phi} |
| |
| \newcommand{\lit}{\ensuremath{\mathscr{L}}} |
| \newcommand{\classvar}{\ensuremath{c}} |
| |
| \newcommand{\lbl}{\ensuremath{\textit{lbl}}} |
| \newcommand{\lbls}{\ensuremath{\textit{lbls}}} |
| \newcommand{\clbl}{\ensuremath{\textit{clbl}}} |
| \newcommand{\clbls}{\ensuremath{\textit{clbls}}} |
| |
| \newcommand{\econt}{\cont_\ensuremath{E}} |
| \newcommand{\acont}{\cont_\ensuremath{A}} |
| \newcommand{\scont}{\cont_\ensuremath{S}} |
| \newcommand{\bcont}{\cont_\ensuremath{B}} |
| \newcommand{\switchcont}{\cont_{\ensuremath{\textit{switch}}}} |
| |
| \newcommand{\funval}[3]{\mathrm{FunctionValue}({#1},\,{#2},\,{#3})} |
| \newcommand{\objval}{\mathrm{ObjectValue}(class, fields)} |
| \newcommand{\obj}{\ensuremath{o}} |
| |
| \newcommand{\formal}{\ensuremath{A}} |
| \newcommand{\formali}[1]{\ensuremath{A_{#1}}} |
| \newcommand{\formals}{\ensuremath{As}} |
| |
| \newcommand{\ncont}{\cont_\ensuremath{N}} |
| \newcommand{\eventloop}{\ensuremath{G}} |
| |
| % Constructor Initializers |
| \newcommand{\Initializer}[1]{\synt{Initializer}(#1)} |
| \newcommand{\FieldInitializer}[1]{\synt{FieldInitializer}(\field, #1)} |
| \newcommand{\LocalInitializer}[1]{\synt{LocalInitializer}(\varmeta, #1)} |
| \newcommand{\SuperInitializer}[2]{\synt{SuperInitializer}(#1,\,#2)} |
| \newcommand{\RedirectingInitializer}[2]{\synt{RedirectingInitializer}(#1,\,#2)} |
| |
| \[ |
| \begin{array}{ccll} |
| \expr, \expri{i} |
| & : & \dexpr & \text{syntactic domain of expressions}\\ |
| \exprs |
| & : & \mlist{\dexpr}\\ |
| |
| \stmt, \stmti{i} |
| & : & \dstmt & \text{syntactic domain of statements}\\ |
| \stmts |
| & : & \mlist{\dstmt} & \text{}\\ |
| |
| \econt |
| & : & \decont & \text{semantic domain of expression continuations}\\ |
| \acont |
| & : & \dacont & \text{semantic domain of application continuations}\\ |
| \scont |
| & : & \dscont & \text{semantic domain of statement continuations}\\ |
| \bcont |
| & : & \dbcont & \text{semantic domain of break continuations}\\ |
| \switchcont |
| & : & \dswitchcont & \text{semantic domain of switch continuations}\\ |
| |
| \lbl & : & \dlbl & \text{semantic domain of labels}\\ |
| \lbls & : & \mlist{\dlbl} \\ |
| \clbl & : & \dclbl & \text{semantic domain of switch labels}\\ |
| \clbls & : & \mlist{\dclbl} \\ |
| |
| \handler |
| & : & \dhandler & \text{syntactic domain of exception handlers} \\ |
| \strace |
| & : & \mlist{\dexpr} & \text{semantic domain of stack traces}\\ |
| \cex |
| & : & \emptyset + \dval & \text{semantic domain of current exception values}\\ |
| \cstrace |
| & : & \emptyset + \mlist{\dexpr} & \text{semantic domain of current exception stack traces}\\ |
| \varmeta |
| & : & \dvar & \text{semantic domain of variables}\\ |
| \loc |
| & : & \dlocation & \text{semantic domain of store locations}\\ |
| \val |
| & : & \dval & \text{semantic domain of values}\\ |
| \vals & : & \mlist{\dval} \\ |
| \vvec & : & \dvector = \mlist{\dval}& \text{semantic domain of vectors}\\ |
| \env |
| & : & \denv & \text{semantic domain of environments}\\ |
| \mainenv |
| & : & \dmenv & \text{semantic domain of main environments}\\ |
| \obj |
| & : & \dobjval & \text{semantic domain of object values}\\ |
| \lit |
| & : & \dlit & \text{syntactic domain of literals}\\ |
| \classvar |
| & : & \dclass & \text{semantic domain of class definitions}\\ |
| \membermeta |
| & : & \dmember & \text{syntactic domain of class members}\\ |
| \idmeta |
| & : & \dident & \text{syntactic domain of identifiers}\\ |
| \typemeta & : & \dtype & \text{semantic domain of Dart types}\\ |
| \formal, \formali{i} & : & \dvardecl & \text{syntactic domain of variable declarations} \\ |
| \formals & : & \dformals = \mlist{\dvardecl} &\text{syntactic domain of formal parameters}\\ |
| \ncont & : & \dncont &\text{semantic domain of event loop continuations}\\ |
| \eventloop & : & \mlist{\dncont} &\text{semantic domain of event loops}\\ |
| \end{array} |
| \] |
| |
| % Metavariables |
| \newcommand{\expressionmeta}{\ensuremath{\mathit{E}}} |
| \newcommand{\expressionsmeta}{\expressionmeta{s}} |
| \newcommand{\variablemeta}{\ensuremath{\mathit{x}}} |
| \newcommand{\boolmeta}{\ensuremath{\mathit{B}}} |
| \newcommand{\integermeta}{\ensuremath{\mathit{I}}} |
| \newcommand{\doublemeta}{\ensuremath{\mathit{D}}} |
| \newcommand{\stringmeta}{\ensuremath{\mathit{S}}} |
| % Metavariables for statements |
| \newcommand{\statementmeta}{\ensuremath{\mathit{\stmt}}} |
| |
| \subsection{Store} |
| \label{subsec:store-definition} |
| |
| The store $s$ is a finite map from location $\loc$ to a value $\val$. |
| The store is a mutable map and should not be confused with a function. |
| A global store is assumed and locations reachable in the current scope are defined by the current environment function |
| \[ |
| s : \dlocation \rightarrow \dval. |
| \] |
| |
| |
| \subsubsection{Locations} |
| |
| The object store is indexed by elements $\loc$ from the domain $\dlocation$. |
| This domain is countably infinite, and we assume that we can generate fresh values from the domain within the abstract machine. |
| It could be represented by natural numbers, for example, but arithmetic on locations is not meaningful. |
| |
| |
| \subsubsection{Dereferencing} |
| \label{subsubsection:dereferecing} |
| |
| \newcommand{\deref}[1]{!#1} |
| The function ``$\deref{}$'' is used to access the value stored in the store at the given location. |
| The location is stored in the environment, or in the list of field locations for object values. |
| ``$\deref{}$'' has an implicit argument which is the store of CESK machine. |
| \begin{align*} |
| &\deref{} \in \dlocation \rightarrow \dval,\\ |
| &\deref{\loc} = \val, \text{ with $\val$ the value in store at location } \loc. |
| \end{align*} |
| |
| |
| \subsubsection{Update} |
| \label{subsubsec:store-update} |
| |
| %\newcommand{\update}[2]{{#1} := {#2}} |
| The operator ``$\update(\loc,\, \val)$'' updates the store at location $\loc \in \dlocation$ with value $\val \in \dval$. |
| It has an implicit operand which is the store of the CESK machine. |
| Upon execution the operator returns a value from domain $\dval$, s.\,t. $\update(\loc,\,\val) = \val$, where $\val$ is the value in the store at location $\loc$. |
| |
| |
| \subsection{Environment} |
| \label{subsec:env-definition} |
| |
| The environment is a function that maps a variable to a location in the store. |
| \[ |
| \env \in \denv = \dvardecl \rightarrow \dlocation. |
| \] |
| |
| When an environment is needed to further execute the program, it is saved by the caller in the corresponding continuation. |
| |
| |
| \subsubsection{Extend} |
| \label{subsubsec:extend-env} |
| |
| Operator ``$\extend$'' creates a new environment by extending the provided environment with new bindings for the variable declarations to fresh locations for each of the provided values. |
| This operator has an implicit operand which is the store of the CESK machine. |
| \begin{align*} |
| &\extend \in \denv \times \mlist{\dvardecl} \times \mlist{\dval} \rightarrow \denv,\\ |
| &\ext{\env}{(\varmeta_{1}, \dots, \varmeta_{n})}{(\val_{1}, \dots, \val_{n})} = \env', |
| \end{align*} |
| |
| \noindent where |
| \begin{align*} |
| & n \in \NN,\\ |
| & (\varmeta_{1}, \dots, \varmeta_{n}) \in \mlist{\dvardecl},\\ |
| & (\val_{1}, \dots, \val_{n}) \in \mlist{\dval},\\ |
| & (\alpha_{1}, \dots, \alpha_{n}) \in \mlist{\dlocation} \text{ --- list of fresh locations in the store},\\ |
| & !\env'(\varmeta) =\begin{cases} |
| !\loc_i = \val_i, & \text{if }\varmeta = \varmeta_i,\\ |
| !\env(\varmeta), &\text{otherwise}. |
| \end{cases} |
| \end{align*} |
| |
| For simpler notation, we allow ``$\extend$'' to be called on single values: $\ext{\env}{\varmeta}{\val}$, which we consider equivalent to calling it on singleton lists: $\ext{\env}{\varmeta :: []}{\val :: []}$. |
| |
| |
| \subsubsection{Variable Lookup} |
| \label{subsubsec:variable-lookup} |
| |
| A variable lookup consists of looking up the location of a variable from the environment with $\loc = \env(\varmeta)$ and reading the stored value $v$ with $\deref{\loc} = \deref{\env(\varmeta)}$ from the store. |
| |
| |
| \subsection{Main Environment} |
| \label{subsec:main-env} |
| |
| \kernel{} supports static and library fields, which are initialized when first accessed and mutations of values stored in these fields are visible in all subsequent execution of statements or evaluation of expressions. |
| To support this feature, we introduce a main environment, denoted as $\mainenv$. |
| |
| \newcommand{\dmainenv}{\textbf{MainEnvironment}} |
| |
| \[\mainenv \in \dmainenv = \dmember \rightarrow \dlocation \] |
| |
| We define the following functions for manipulating $\mainenv$: |
| |
| \subsubsection{Contains} |
| We define the function $\contains$ as follows: |
| \begin{align*} |
| \contains &\in \dmainenv \times \dmember \rightarrow \dsembool\\ |
| \contains(\mainenv, x) &=\begin{cases} |
| \true &\text{ if }x \in \dom(\mainenv),\\ |
| \false &\text{ otherwise} |
| \end{cases} |
| \end{align*} |
| where $\dom(\mainenv)$ is the domain of the environment $\mainenv$, i.e. the set of members for which $\mainenv$ is defined. |
| |
| We will use `\contains` as a proposition in the transition steps below, since the value produced is not used alongside the values from the semantic domains. |
| |
| \subsubsection{Extend} |
| We define the function extend as follows: |
| \begin{align*} |
| &\extend \in \dmainenv \times \dmember \times \dval \rightarrow \denv\\ |
| &\extend(\mainenv, x, \val) = \mainenv',\\ |
| &\text{where }\\ |
| &\forall y \in \dom(\mainenv) \cup \{x\},\,\mainenv'(y) =\begin{cases} |
| \loc &\text{ if } y = x,\\ |
| \mainenv(y) &\text{ otherwise}\\ |
| \end{cases}\\ |
| &\text{and $\loc$ is a fresh location that stores the value $\val$.} |
| \end{align*} |
| |
| This environment is visible during the execution of a \kernel{} program, therefore it should be in the left and right-hand side of all the transition presented in the paper. |
| In order to simplify the transitions, we assume the main environment is implicit. |
| |
| For a rule $C_1 \Rightarrow C_2$ that defines the transition from configuration $C_1$ to configuration $C_2$, we explicitly mention when the main environment in the resulting configuration $C_2$ is not the same as the one in the previous configuration $C_1$. |
| |
| \subsubsection{Static and Library Field Lookup} |
| \label{subsubsec:static-field-lookup} |
| |
| A static and library field lookup for field $\field$ consists of looking up the location of the static field from the main environment with $\loc = \mainenv(\field)$ and reading the stored value $v$ with $\deref{\loc} = \deref{\mainenv(\field)}$ from the store. |
| |
| |
| \subsection{Values} |
| \label{sec:values} |
| |
| Values in \kernel{} fall into two categories: $\dvector$ values and $\dobjval$ values. |
| Values are irreducible terms, i.e, the result of the evaluation of expressions. |
| Only object values may be in the image of the store. |
| |
| \subsubsection{Vector Values} |
| \label{subsubsec:vector-values} |
| |
| \kernel{} has limited support for arrays without bounds checking via $\dvector$s. |
| The step function for the CESK machine is not defined for operations that access an element vector outside its bounds. |
| $\dvector$s cannot be introduced by any construct present in \dart{} itself, but rather are introduced only by \kernel{} transformations which can ensure they are only used in a safe manner. |
| |
| \subsubsection{Literals} |
| |
| Some objects from primitive types contain a literal value and a specific class corresponding to the literal's type. |
| The different types of literal values are: |
| \[\dlit = \dsemint + \dsembool + \dsemdouble + \dsemlist + \dsemmap + \dsemstring + \dsemsymbol + \dtype.\] |
| |
| Literal values are special values that store the specific payload and an associated class. |
| Each of the specific literal values contains predefined operators and methods, whose semantics are elided here. |
| |
| \subsubsection{Class} |
| \label{subsubsec:class} |
| |
| A $\dclass$ encodes a class definition in \kernel{}. |
| |
| \begin{align*} |
| \dclass &= (\emptyset + \dclass) \times \mlist{\dclass} \times (\dident \mapsto \dmember)\\ |
| \dmember &= \mathbf{Getter} + \mathbf{Setter} + \mathbf{Method} \\ |
| \mathbf{Getter} &= \NN + \dstmt \\ |
| \mathbf{Setter} &= \NN + \dformals \times \dstmt \\ |
| \mathbf{Method} &= \dformals \times \dstmt |
| \end{align*} |
| |
| A class definition contains a reference to the superclass (none only in the case of the ``Object'' class), a list of interface classes and a finite map from identifiers to members which provides dynamic dispatch. |
| The natural-indexed getters and setters correspond to the case where a field should be modified directly, and the number provides the index into an instance's list of locations. |
| |
| Although constructor definitions are included in the class definition, they are not presented here because the same syntax nodes are directly referenced by the expression form for constructor invocation. |
| |
| For accessing the superclass component of elements in the domain $\dclass$ we define: |
| \begin{align*} |
| \superclass &\in \dclass \rightarrow \dclass,\\ |
| \superclass(c_1) &= \pi_1(c_1) = c_2, \text{ where $c_2 \in \dclass$ is the first component of $c_1 \in \dclass$} |
| \end{align*} |
| |
| For accessing the members component of elements in the domain $\dclass$, we define: |
| \begin{align*} |
| \members &\in \dclass \rightarrow (\dident \mapsto \dmember),\\ |
| \members(c) &= \pi_3(c), \text{where $c \in \dclass$} |
| \end{align*} |
| |
| For looking up a member, given its identifier $\idmeta \in \dident$, we define: |
| \begin{align*} |
| \lookupMember &\in \dclass \times \dident \rightarrow \dmember,\\ |
| \lookupMember(c, \, \idmeta) &= \members(c)(\idmeta), \text{ where $c \in \dclass, \idmeta \in \dident$} |
| \end{align*} |
| |
| \subsubsection{Object Values} |
| \label{subsec:object-values} |
| |
| Object values are composed of a reference to a class definition, which is shared across all instances of that object, and a list of locations which identify the values of the fields for a specific instance. |
| \[ |
| \dobjval = \dclass \times \mlist{\dlocation} |
| \] |
| |
| We define the following function for accessing the class component of an element in $\dobjval$: |
| \begin{align*} |
| \class &\in \dobjval \rightarrow \dclass,\\ |
| \class(\val) &= \pi_1(\val) = c, \text{ where $c \in \dclass$ is the first component of $\val \in \dobjval$} |
| \end{align*} |
| |
| |
| We define the following function for accessing the location of a field at position $i \in \NN$ in $\dobjval$: |
| \begin{align*} |
| \getfield &\in \dobjval \times \NN \rightarrow \dlocation,\\ |
| \getfield(\val, i) &= \pi_2(\val)[i] = \loc, \text{ where $\pi_2(\val) \in \mlist{\dlocation}$ and $\pi_2(\val)[i]$ is the location at position $i \in \NN$} |
| \end{align*} |
| |
| \subsubsection{Function Values} |
| \label{subsec:function-values} |
| Function values capture the body, formals and the environment in which a function was created. |
| To support recursive functions, we add a location component to the function value and store the environment in it. |
| This allows us to modify the environment and add a binding to a location containing the function value for local functions. |
| \[ |
| \dfunval : \dformals \times \dstmt \times \denv |
| \] |
| |
| |
| \section{\kernel{} Syntax} |
| \label{sec:definitions} |
| |
| |
| \subsection{Expressions} |
| \label{sec:expr-syntax} |
| |
| |
| % Syntax |
| \newcommand{\VariableGet}[1]{#1} |
| \newcommand{\VariableSet}[2]{#1=#2} |
| |
| \todo{kmillikin: Names should not ignore the library.} |
| \newcommand{\PropertyGet}[2]{#1.#2} |
| \newcommand{\PropertySet}[3]{#1.#2=#3} |
| |
| \newcommand{\DirectPropertyGet}[2]{#1.\{#2\}} |
| \newcommand{\DirectPropertySet}[3]{#1.\{#2\}=#3} |
| |
| \newcommand{\SuperPropertyGet}[1]{\synt{super}.#1} |
| \newcommand{\SuperPropertySet}[2]{\synt{super}.#1=#2} |
| |
| \newcommand{\StaticGet}[1]{\{#1\}} |
| \newcommand{\StaticSet}[2]{\{#1\}=#2} |
| |
| %% MethodInvocation |
| \newcommand{\InstanceMethodInvocation}[3]{#1.#2(#3)} |
| %% DirectMethodInvocation |
| \newcommand{\DInstanceMethodInvocation}[3]{#1.\{#2\}(#3)} |
| %% SuperMethodInvocation |
| \newcommand{\SuperMethodInvocation}[2]{\synt{super}.#1(#2)} |
| %% StaticInvocation |
| \newcommand{\StaticInvocation}[2]{#1(#2)} |
| %% ConstructorInvocation |
| \newcommand{\New}[2]{\new\, #1\,(#2)} |
| |
| \newcommand{\Not}[1]{\synt{!}#1} |
| \newcommand{\AndExpression}[2]{#1\,\synt{\&\&}\,#2} |
| \newcommand{\OrExpression}[2]{#1\,\synt{||}\,#2} |
| \newcommand{\ConditionalExpression}[3]{#1\,\synt{?}\,#2\,\synt{:}\,#3} |
| |
| %% StringConcatenation |
| \newcommand{\StringConcatenation}[2]{#1\,\dots\,#2} |
| |
| \newcommand{\IsExpression}[2]{#1\,\synt{is}\,#2} |
| \newcommand{\AsExpression}[2]{#1\,\synt{as}\,#2} |
| |
| %% SymbolLiteral |
| %% TypeLiteral |
| |
| |
| %% ListLiteral |
| %% MapLiteral |
| |
| \newcommand{\AwaitExpression}[1]{\synt{await\,#1}} |
| |
| %% FunctionExpression |
| |
| \newcommand{\StringLiteral}[1]{#1} |
| \newcommand{\IntLiteral}[1]{#1} |
| \newcommand{\DoubleLiteral}[1]{#1} |
| \newcommand{\BoolLiteral}[1]{#1} |
| \newcommand{\NullLiteral}{\nnull} |
| \newcommand{\Let}[3]{\synt{let}\,#1\synt{=}#2\,\synt{in}\,#3} |
| |
| %% LoadLibrary |
| %% CheckLibraryIsLoaded |
| %% VectorCreation |
| %% VectorGet |
| %% VectorSet |
| %% VectorCopy |
| %% ClosureCreation |
| %% TypeInstantiation |
| |
| \[ |
| \begin{array}{rl} |
| \expressionmeta \in \dexpr ::= |
| & \VariableGet{\variablemeta} \\ |
| & \VariableSet{\variablemeta}{\expressionmeta} \\ |
| & \PropertyGet{\expressionmeta}{\idmeta} \\ |
| & \PropertySet{\expressionmeta_0}{\idmeta}{\expressionmeta_1} \\ |
| & \DirectPropertyGet{\expressionmeta}{\membermeta} \\ |
| & \DirectPropertySet{\expressionmeta_0}{\membermeta}{\expressionmeta_1} \\ |
| & \SuperPropertyGet{\idmeta} \\ |
| & \SuperPropertySet{\idmeta}{\expressionmeta} \\ |
| & \StaticGet{\membermeta} \\ |
| & \StaticSet{\membermeta}{\expressionmeta} \\ |
| & \Not{\expressionmeta} \\ |
| & \AndExpression{\expressionmeta_0}{\expressionmeta_1} \\ |
| & \OrExpression{\expressionmeta_0}{\expressionmeta_1} \\ |
| & \ConditionalExpression{\expressionmeta_0}{\expressionmeta_1}{\expressionmeta_2} \\ |
| & \New{\synt{Q}}{\expressionmeta*} \\ |
| & \IsExpression{\expressionmeta}{\typemeta} \\ |
| & \AsExpression{\expressionmeta}{\typemeta} \\ |
| & \this \\ |
| & \Rethrow \\ |
| & \Throw{\expressionmeta} \\ |
| & \AwaitExpression{\expressionmeta} \\ |
| & \lit \\ |
| & \NullLiteral \\ |
| & \Let{\variablemeta}{\expressionmeta_0}{\expressionmeta_1} \\ |
| \end{array} |
| \] |
| |
| |
| \subsection{Statements} |
| \label{subsec:stmt-syntax} |
| |
| % InvalidStatement |
| \newcommand{\ExpressionStatement}[1]{\{\, #1\, \}} |
| \newcommand{\Block}[1]{\{\, #1\, \}} |
| \newcommand{\EmptyStatement}{\{\}} |
| |
| % AssertStatement |
| \newcommand{\LabeledStatement}[2]{#1\synt{:}\, #2} |
| \newcommand{\BreakStatement}[1]{\synt{break}\, #1} |
| \newcommand{\WhileStatement}[2]{\synt{while}\, \synt{(}#1\synt{)}\, #2} |
| \newcommand{\DoStatement}[2]{\synt{do}\, #1\, \synt{while}\, \synt{(}#2\synt{)}} |
| \newcommand{\ForStatement}[4]{\synt{for}\, \synt{(}\,#1\synt{;}\, #2\synt{;}\, #3\,\synt{)}\, #4} |
| \newcommand{\ForInStatement}[3]{\synt{for}\,\synt{(}#1\,\synt{in}\,#2\synt{)}\,#3} |
| |
| \newcommand{\SwitchStatement}[2]{\synt{switch}\,\synt{(}#1\synt{)}\,#2} |
| \newcommand{\ContinueSwitchStatement}[1]{\synt{continue}\,#1} |
| \newcommand{\IfStatement}[3]{\synt{if}\,\synt{(}#1\synt{)}\,#2\,\synt{else}\,#3} |
| \newcommand{\ReturnStatement}[1]{\synt{return}\,#1} |
| |
| \newcommand{\TryCatch}[2]{\synt{try}\,#1\,\synt{catch}\,#2} |
| \newcommand{\TryFinally}[2]{\synt{try}\,#1\,\synt{finally}\,#2} |
| |
| \newcommand{\Yield}[1]{\synt{yield}\,#1} |
| |
| \newcommand{\VarDeclaration}[2]{\synt{var}\,#1\synt{=}#2} |
| \newcommand{\FunctionDeclaration}[5]{#1\,#2\synt{(}\,#3\,\synt{)}\,#4\,#5} |
| |
| \[ |
| \begin{array}{rl} |
| |
| \statementmeta \in \dstmt ::= |
| & \ExpressionStatement{\expressionmeta} \\ |
| & \Block{\statementmeta{s}} \\ |
| & \EmptyStatement \\ |
| & \LabeledStatement{\lbl}{\statementmeta} \\ |
| & \BreakStatement{\lbl} \\ |
| & \WhileStatement{\expressionmeta}{\statementmeta} \\ |
| & \DoStatement{\statementmeta}{\expressionmeta} \\ |
| & \ForStatement{\varmeta{s}}{\expressionmeta}{\expressionsmeta}{\statementmeta} \\ |
| & \ForInStatement{\varmeta}{\expressionmeta}{\statementmeta} \\ |
| & \SwitchStatement{\expressionmeta}{\tt{SCs}} \\ |
| & \ContinueSwitchStatement{\statementmeta} \\ |
| & \IfStatement{\expressionmeta}{\statementmeta_1}{\statementmeta_2} \\ |
| & \ReturnStatement{\expressionmeta} \\ |
| & \ReturnStatement{} \\ |
| & \TryCatch{\statementmeta}{\tt{CCs}} \\ |
| & \TryFinally{\statementmeta_1}{\statementmeta_2} \\ |
| & \Yield{\expressionmeta} \\ |
| & \VarDeclaration{\idmeta}{\expressionmeta} \\ |
| & \FunctionDeclaration{\typemeta}{\idmeta}{\formals}{}{\stmt} \\ |
| |
| \end{array} |
| \] |
| \todo{Add sync*/async/async* marker and type parameters} |
| |
| \section{CESK Machine States} |
| \subsection{Configurations} |
| \label{subsec:cesk-configs} |
| |
| The state space of the CESK machine contains various kinds of configurations. |
| Configurations contain different components and the transition step dispatches to the next configuration based on one of the components of the configuration. |
| |
| % Named Configuration for CESK transitions |
| \newcommand{\breakconf}[1]{\confsingle{#1}_{\mathrm{breakCont}}} |
| \newcommand{\switchconf}[1]{\confsingle{#1}_{\mathrm{switchCont}}} |
| \newcommand{\contconf}[2]{\confpair{#1}{#2}_{\mathrm{cont}}} |
| \newcommand{\scontconf}[2]{\confpair{#1}{#2}_{\mathrm{scont}}} |
| \newcommand{\acontconf}[2]{\confpair{#1}{#2}_{\mathrm{acont}}} |
| \newcommand{\throwconf}[3]{\conftriple{#1}{#2}{#3}_{\mathrm{throw}}} |
| \newcommand{\evallistconf}[6]{\langle{#1},\,{#2},\,{#3},\handler,\,{#4},\,{#5},\,{#6}\rangle_{\mathrm{evalList}}} |
| \newcommand{\evalconf}[6]{\langle{#1},\,{#2},\,{#3},\handler,\,{#4},\,{#5},\,{#6}\rangle_{\mathrm{eval}}} |
| \newcommand{\execconf}[9]{\langle{#1},\,{#2},\,{#3},\,{#4},\,{#5},\,{#6},\,{#7},\,{#8},\,{#9}\rangle_{\mathrm{exec}}} |
| \newcommand{\eventconf}[2]{\langle{#1},\,{#2}\rangle_{\mathrm{event}}} |
| |
| % Transition |
| \todo{dmitryas: Add G (event loop) to all configurations.} |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\evalconf{\expr}{\env}{st}{cex}{cst}{\econt} & :\quad & \text{EvalConfiguration} \label{config:eval}\\ |
| &\evallistconf{\exprs}{\env}{st}{cex}{cst}{\acont} & :\quad & \text{EvalListConfiguration} \label{config:evallist}\\ |
| &\execconf{\stmt}{\env}{\lbls}{\clbls}{\strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont} & :\quad & \text{ExecConfiguration} \label{config:exec}\\ |
| &\contconf{\econt}{\val} & :\quad & \text{ValuePassingConfiguration} \label{config:econt}\\ |
| &\acontconf{\acont}{\vals} & :\quad & \text{ApplicationConfiguration} \label{config:acont}\\ |
| &\scontconf{\scont}{\env} & :\quad & \text{ForwardConfiguration} \label{config:scont}\\ |
| &\throwconf{\handler}{\val}{\strace} & :\quad & \text{ThrowConfiguration} \label{config:throw}\\ |
| &\breakconf{\bcont} & :\quad & \text{BreakConfiguration} \label{config:bcont}\\ |
| &\switchconf{\switchcont} & :\quad & \text{SwitchConfiguration} \\ |
| &\eventconf{\ncont}{\eventloop} & :\quad & \text{EventLoopConfiguration} |
| \label{config:switchcont} |
| \end{align} |
| \caption{States for the CESK machine} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{EvalConfiguration} |
| \label{subsubsec:evalconfig} |
| |
| The configuration EvalConfiguration is shown in \ref{config:eval}. |
| The transition step for this configuration dispatches on the expression component, $\expr$. |
| With one transition step of the CESK-transition function, from the EvalConfiguration the next configuration can be one of the following: |
| |
| \begin{itemize} |
| \item ValuePassingConfiguration, when the current expression evaluates to a value in one step. |
| \item ExecConfiguration, when the current expression results with an invocation, i.e. execution of statement body of a getter. |
| Note that for other invocations, we first evaluate the receiver for instance invocations, or the arguments for static or constructor invocations. |
| \item EvalListConfiguration, when the current expression implies evaluation of a list of expressions. |
| \item ThrowConfiguration, when the current expression throws, i.e. is a throw expression. |
| \item EvalConfiguration, otherwise. |
| \end{itemize} |
| |
| |
| \subsubsection{EvalListConfigruation} |
| \label{subsubsec:evallistconfig} |
| |
| The configuration EvalListConfiguration is shown in Figure~\ref{config:evallist}. |
| The transition step for this configuration dispatches on the expression list, $\exprs$. |
| With one step of the CESK-transition function, from EvalListConfifuration the next configuration is either EvalConfiguration, when $\exprs \neq []$, or ApplicationConfiguration, otherwise. |
| |
| |
| \subsubsection{ExecConfiguration} |
| \label{subsubsec:execconfig} |
| |
| The configuration ExecConfiguration is shown in Figure~\ref{config:exec}. |
| The transition step dispatches on the statement, $\stmt$. |
| The next configuration is either EvalConfiguration or ExecConfiguration. |
| |
| |
| \subsubsection{ValuePassingConfiguration} |
| \label{suubsubsec:valuepassingconfig} |
| |
| The configuration ValuePassingConfiguration is shown in Figure~\ref{config:econt}. |
| The transition step applies the expression continuation component to its value component. |
| The expression continuation produces the next configuration. |
| |
| |
| \subsubsection{ApplicationConfiguration} |
| \label{subsubsec:applicationconfig} |
| |
| The configuration ApplicationConfiguration is shown in Figure~\ref{config:acont}. |
| The transition step applies the application continuation component to its list of values component. |
| The application continuation produces the next configuration. |
| |
| |
| \subsubsection{ForwardConfiguration} |
| \label{subsubsec:forwardconfig} |
| |
| The configuration ForwardConfiguration is shown in Figure~\ref{config:scont}. |
| The transition step applies the statement continuation component to its environment component. |
| The statement continuation produces the next configuration. |
| |
| |
| \subsubsection{ThrowCongfiguration} |
| \label{subsubsec:throwconfig} |
| |
| The configuration ThrowConfiguration is shown in Figure~\ref{config:throw}. |
| The transition step applies the exception handler. |
| The next configuration is: |
| |
| \begin{itemize} |
| \item ThrowConfiguration, when the exception is not handled by the first catch clause of a catch handler. |
| \item ExecConfiguration, for the statement body of the matching catch or the finally statement, when no catch clauses are present. |
| \end{itemize} |
| |
| |
| \subsubsection{BreakConfiguration} |
| \label{subsubsec:breakconfig} |
| |
| The configuration BreakConfiguration is shown in Figure~\ref{config:bcont}. |
| The transition step applies the break continuation component. |
| The next configuration is ForwardConfiguration. |
| |
| |
| \subsubsection{SwitchConfiguration} |
| \label{subsubsec:switchconfig} |
| |
| The configuration SwitchConfiguration is shown in Figure~\ref{config:switchcont}. |
| The transition step applies the switch continuation component. |
| The next configuration is ExecConfiguration. |
| |
| |
| \subsection{Continuations} |
| \label{subsec:continuations-definition} |
| |
| Continuations represent the instructions for execution of statements or evaluation of expressions. |
| They capture the information needed to resume the execution of the program. |
| There are various types of continuations depending on the state for evaluation of an expression or execution of a statement. |
| |
| |
| \subsubsection{Expression Continuations} |
| \label{subsubsec:expression-continuations} |
| |
| Expression continuations, $\econt$, capture the steps after the evaluation of a given expression. |
| They accept a value and produce the next configuration. |
| |
| There are various kinds of configurations, but two more general types can be distinguished: |
| |
| \begin{itemize} |
| \item Continuations with holes, i.e. expressions to be evaluated\\ |
| Expression continuations with expressions will produce EvalConfiguration for evaluation of the next expression. |
| Note that some continuation will not evaluate the captured expression, when this is not necessary (e.g., \eqref{eval:and}). |
| |
| \item Continuations without holes\\ |
| Continuations without holes dispatch on the provided value and produce the next configuration, a ValuePassingConfiguration. |
| |
| \end{itemize} |
| |
| We suffix the names of expression continuations with ``$K$''. |
| The different expression continuations are shown in Figure~\ref{figure:econts}. |
| |
| \newcommand{\ExceptionHandlersRest}{\handler,\,\cstrace,\,\cex} |
| \newcommand{\ExceptionHandlers}{\strace,\,\handler,\,\cstrace,\,\cex} |
| % Continuations |
| \newcommand{\VarSetK}[4]{\mathrm{VarSetEK}({#1},\,{#2},\,{#3},\,{#4})} |
| \newcommand{\ExpressionsK}[3]{\mathrm{ExpressionsEK}({#1},\,{#2},\,\ExceptionHandlers,\,{#3})} |
| |
| \newcommand{\NotK}[1]{\mathrm{NotEK}({#1})} |
| \newcommand{\AndK}[3]{\mathrm{AndEK}({#1},\,{#2},\,\ExceptionHandlers,\,{#3})} |
| \newcommand{\OrK}[3]{\mathrm{OrEK}({#1},\,{#2},\,\ExceptionHandlers,\,{#3})} |
| \newcommand{\ConditionalK}[4]{\mathrm{ConditionalEK}({#1},\,{#2},\,{#3},\,\ExceptionHandlers,\,{#4})} |
| |
| \newcommand{\LetK}[4]{\mathrm{LetEK}({#1},\,{#2},\,{#3},\,\ExceptionHandlers,\,{#4})} |
| |
| \newcommand{\IsExpressionK}{\mathrm{IsExpressionEK}(\tt{T},\,\econt)} |
| \newcommand{\AsExpressionK}{\mathrm{AsExpressionEK}(\tt{T},\,\strace,\,\handler,\,\econt)} |
| |
| \newcommand{\StaticGetK}{\mathrm{StaticGetEK}(\membermeta,\,\econt)} |
| \newcommand{\StaticSetK}{\mathrm{StaticSetEK}(\membermeta,\,\econt)} |
| \newcommand{\PropertyGetK}{\mathrm{PropertyGetEK}(\idmeta,\,\ExceptionHandlers,\,\econt)} |
| \newcommand{\PropertySetK}{\mathrm{PropertySetEK}(\idmeta,\,\expressionmeta_1,\,\env,\,\ExceptionHandlers,\,\econt)} |
| \newcommand{\PropertySetVK}{\mathrm{PropertySetValueEK}(\val_0,\,\idmeta,\,\ExceptionHandlers,\,\econt)} |
| \newcommand{\DPropertyGetK}{\mathrm{DPropertyGetEK}(\membermeta,\,\ExceptionHandlers,\,\econt)} |
| \newcommand{\DirectPropertySetK}{\mathrm{DPropertySetEK}(\membermeta,\,\expressionmeta_1,\,\env,\,\ExceptionHandlers,\,\econt)} |
| \newcommand{\DPropertySetVK}{\mathrm{DPropertySetValueEK}(\val_0,\,\membermeta,\,\ExceptionHandlers,\,\econt)} |
| \newcommand{\SuperPropertySetK}{\mathrm{SuperPropertySetEK}(\idmeta,\,\env,\,\ExceptionHandlers,\,\econt)} |
| |
| \newcommand{\InstanceMethodK}[1]{\mathrm{InstanceMethodK(\expressionsmeta,\,\idmeta,\,\env,\,#1,\,\ExceptionHandlersRest,\,\econt)}} |
| \newcommand{\DInstanceMethodK}[1]{\mathrm{DInstanceMethodEK}(\expressionsmeta,\,\membermeta,\,\env,\,#1,\,\ExceptionHandlersRest,\,\econt)} |
| \newcommand{\VarDeclK}[3]{\mathrm{VarDeclarationEK}({#1},\,{#2},\,{#3})} |
| \newcommand{\IfCondK}[2]{\mathrm{IfConditionEK}({#1},\,{#2},\,\env,\,\lbls,\,\clbls,\,\handler,\,\cstrace,\,\cex,\,\econt,\,\scont)} |
| \newcommand{\SwitchK}[2]{\mathrm{SwitchEK}({#1},\,\env,\,\lbls,\,{#2},\,\strace,\,\handler,\,\cstrace,\,\cex,\,\econt,\,\scont)} |
| |
| \newcommand{\WhileCondK}{\mathrm{WhileCondEK}(\expr,\,\stmt,\,\env,\,\lbls,\,\clbls,\,\strace,\,\handler,\,\cstrace,\,\cex,\,\econt,\,\scont)} |
| \newcommand{\InitializerK}[4]{\mathrm{InitializerEK}({#1},\,{#2},\,{#3},\,\strace,\,\handler,\,\cstrace,\,\cex,\,{#4})} |
| \newcommand{\InitK}[3]{\mathrm{InitEK}({#1},\,{#2},\,\strace,\,\handler,\,\cstrace,\,\cex,\,{#3})} |
| \newcommand{\InitializerListEK}[5]{\mathrm{InitializerListEK}({#1},\,{#2},\,{#3},\,{#4},\,\strace,\,\handler,\,\cstrace,\,\cex,\,{#5})} |
| \newcommand{\FinallyK}[1]{\mathrm{FinallyEK}({#1},\,\env,\,\lbls,\,\clbls,\,\strace,\,\handler,\,\econt)} |
| \newcommand{\FinallyReturnK}[1]{\mathrm{FinallyReturnEK}({#1},\,\env,\,\lbls,\,\clbls,\,\strace,\,\handler,\,\econt)} |
| |
| \newcommand{\ForCondK}{\mathrm{ForConditionEK}(\varmeta{s},\, \expressionmeta,\, \exprs,\, \statementmeta,\, \env,\, \env',\, \lbls,\, \clbls,\, \handler,\, \cstrace,\, \cex,\, \econt,\, \scont)} |
| \newcommand{\ExpressionK}[2]{\mathrm{ExpressionEK}({#1},\,{#2})} |
| |
| \newcommand{\AsyncReturnEK}[1]{\mathrm{AsyncReturnEK}({#1})} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\VarSetK{\idmeta}{\env}{\ExceptionHandlers}{\econt} \label{econt:varset}\\ |
| &\ExpressionsK{\exprs}{\env}{\acont} \label{econt:expressions}\\ |
| &\NotK{\econt} \label{econt:not}\\ |
| &\AndK{\expressionmeta}{\ExceptionHandlers}{\econt} \label{econt:and}\\ |
| &\OrK{\expressionmeta}{\ExceptionHandlers}{\econt} \label{econt:or}\\ |
| &\ConditionalK{\expressionmeta_1}{\expressionmeta_2}{\ExceptionHandlers}{\econt} \label{econt:cond}\\ |
| &\LetK{\varmeta}{\expressionmeta}{\ExceptionHandlers}{\econt} \label{econt:let}\\ |
| &\IsExpressionK \label{econt:is}\\ |
| &\AsExpressionK \label{econt:as}\\ |
| &\StaticGetK \label{econt:static-get}\\ |
| &\StaticSetK \label{econt:static-set}\\ |
| &\DPropertyGetK \label{econt:dproperty-get}\\ |
| &\PropertySetK \label{econt:property-set}\\ |
| &\PropertySetVK \label{econt:property-set}\\ |
| &\DPropertyGetK \label{econt:dproperty-set}\\ |
| &\DPropertySetVK \label{econt:dproperty-set-v}\\ |
| &\SuperPropertySetK \label{econt:super-property-set}\\ |
| &\InstanceMethodK{\strace} \label{econt:instance-method}\\ |
| &\DInstanceMethodK{\strace} \label{econt:dinstance-method}\\ |
| &\VarDeclK{\idmeta}{\env}{\scont} \label{econt:var-decl}\\ |
| &\IfCondK{\expressionmeta_1}{\expressionmeta_2} \label{econt:if-cond}\\ |
| &\ForCondK \label{econt:for-cond}\\ |
| &\ExpressionK{\scont}{\env} \label{econt:expression}\\ |
| &\InitializerListEK{Q}{i}{\loc}{\env}{\scont} \label{econt:initializer-list}\\ |
| &\AsyncReturnEK{\econt} |
| \end{align} |
| \caption{Expression Continuations} |
| \label{figure:econts} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Statement Continuations} |
| \label{subsubsec:statement-continuations} |
| |
| Statement continuations, $\scont$, capture the steps after execution of a statement. |
| They accept an environment and produce the next configuration. |
| Statements in a block expressions can extend the environment function and this is visible to the subsequent statements in the same block. |
| For other types of statement configuration, the environment is ignored. |
| |
| We suffix the names of statement continuations with ``$SK$''. |
| The different statement continuations are shown in Figure~\ref{figure:sconts}. |
| |
| \newcommand{\ExitSK}[1]{\mathrm{ExitSK}(\econt,\,#1)} |
| \newcommand{\BlockSK}[2]{\mathrm{BlockSK}({#1},\,{#2},\,\lbls,\,\clbls,\,\handler,\,\cstrace,\,\cex,\,\econt,\,\scont)} |
| \newcommand{\WhileSK}{\mathrm{WhileSK}(\expr,\,\stmt,\,\env,\,\lbls,\,\clbls,\,\handler,\,\cstrace,\,\cex,\,\econt,\,\scont)} |
| \newcommand{\BodySK}[3]{\mathrm{BodySK}({#1},\,{#2},\,\strace,\,\handler,\,\cstrace,\,\cex,\,{#3})} |
| \newcommand{\NewSK}[2]{\mathrm{NewSK}({#1},\,{#2})} |
| \newcommand{\FinallySK}[1]{\mathrm{FinallySK}({#1},\,\env,\,\lbls,\,\clbls,\,\strace,\,\handler,\,\econt,\,\scont)} |
| \newcommand{\RethrowSK}[3]{\mathrm{RethrowSK}({#1},\,{#2},\,{#3})} |
| \newcommand{\ForSK}{\mathrm{ForSK}(\varmeta{s},\, \expressionmeta,\, \exprs,\, \statementmeta,\, \env,\, \env',\, \lbls,\, \clbls,\, \handler,\, \cstrace,\, \cex,\, \econt,\, \scont)} |
| \newcommand{\WhileCondSK}{\mathrm{WhileCondSK}(\expr,\,\stmt,\,\env,\,\lbls,\,\clbls,\,\handler,\,\cstrace,\,\cex,\,\econt,\,\scont)} |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\ExitSK{\val} \label{scont:exit}\\ |
| &\BlockSK{\stmts}{\env} \label{scont:block}\\ |
| &\WhileSK \label{scont:while}\\ |
| &\BodySK{\stmt}{\env}{\scont} \label{scont:body}\\ |
| &\NewSK{\econt}{\loc} \label{scont:new}\\ |
| &\FinallySK{\stmt} \label{scont:finally}\\ |
| &\RethrowSK{\val}{\strace}{\handler} \label{scont:rethrow}\\ |
| &\ForSK \label{scont:for}\\ |
| &\WhileCondSK \label{scont:while} |
| \end{align} |
| \caption{Statement Continuations} |
| \label{figure:sconts} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Application Continuation} |
| \label{subsubsec:application-continuation} |
| |
| Application continuations, $\acont$, capture the application of a list of values resulting from the evaluation of list of expressions. |
| |
| \newcommand{\ValueA}[2]{\mathrm{ValueA}({#1},\,{#2})} |
| \newcommand{\StringConcatenationA}{\mathrm{StringConcatenationA(\econt)}} |
| \newcommand{\SuperMethodA}[1]{\mathrm{SuperMethodA}(\idmeta,\,\env,\,#1,\,\ExceptionHandlersRest,\,\econt)} |
| \newcommand{\StaticInvA}[4]{\mathrm{StaticInvocationA}({#1},\,{#2},\,{#3},\,\ExceptionHandlersRest,\,{#4})} |
| \newcommand{\DInstanceMethodA}{\mathrm{DInstanceMethodA}(\membermeta,\,\val,\,\ExceptionHandlers,\,\econt)} |
| \newcommand{\FieldsA}[4]{\mathrm{InstanceFieldsA}({#1},\,{#2},\,{#3},\,\strace,\,\handler,\,\cstrace,\,\cex,\,{#4})} |
| \newcommand{\SuperA}[3]{\mathrm{SuperA}({#1},\,{#2},\,\strace,\,\handler,\,\cstrace,\,\cex,\,{#3})} |
| \newcommand{\ConstructorA}[3]{\mathrm{ConstructorA}({#1},\,{#2},\,\handler,\,\cstrace,\,\cex,\,{#3})} |
| \newcommand{\RedirectingA}[3]{\mathrm{RedirectingA}({#1},\,{#2},\,\strace,\,\handler,\,\cstrace,\,\cex,\,{#3})} |
| \newcommand{\ForInitA}[1]{\mathrm{ForInitA}(\varmeta{s},\, #1,\, \exprs,\, \statementmeta,\, \env,\, \lbls,\, \clbls,\, \handler,\, \cstrace,\, \cex,\, \econt,\, \scont)} |
| \newcommand{\ForUpdatesA}[2]{\mathrm{ForUpdatesA}(\varmeta{s},\, #1,\, \exprs,\, \statementmeta,\, \env,\, #2,\, \lbls,\, \clbls,\, \handler,\, \cstrace,\, \cex,\, \econt,\, \scont)} |
| \newcommand{\InstanceMethodA}{\mathrm{InstanceMethodA(\idmeta,\,\val,\,\strace,\,\handler,\,\cstrace,\,\cex,\,\econt)}} |
| |
| We use the application continuation $\ValueA{\acont}{\val}$, capturing a value and an application continuation, as application that adds a value to the list of values to eventually used by an application continuation that produces a configuration other than ApplicationConfiguration. |
| We suffix the names of application continuations with ``$A$''. |
| The different application continuations are shown in Figure~\ref{figure:acont}. |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\ValueA{\val}{\acont} \label{acont:value}\\ |
| &\StringConcatenationA \label{acont:stringconcat}\\ |
| &\ForInitA{\expressionmeta} \label{acont:forinit}\\ |
| &\ForUpdatesA{\expressionmeta}{\env'} \label{acont:forupdates}\\ |
| &\SuperMethodA{\strace} \label{acont:supermethod}\\ |
| &\DInstanceMethodA \label{acont:staticinv}\\ |
| &\FieldsA{Q}{\loc}{\env}{\scont} \label{acont:fields}\\ |
| &\ConstructorA{Q}{\strace}{\econt} \label{acont:constructor}\\ |
| &\SuperA{Q}{\loc}{\scont} \label{acont:super}\\ |
| &\RedirectingA{Q}{\loc}{\scont} \label{acont:redirecting} |
| \end{align} |
| \caption{Application Continuations} |
| \label{figure:acont} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Break Continuations} |
| \label{subsubsec:break-continuations} |
| |
| Break continuations, $\bcont$, capture the steps to be executed when a break to a given label is encountered. |
| The different break continuations are shown in Figure~\ref{figure:breakcont}. |
| \newcommand{\Break}[2]{\mathrm{Break}(#1,\,#2)} |
| \newcommand{\FinallyBreak}[2]{\mathrm{FinallyBreak}({#1},\,\env,\,\lbls,\,\clbls,\,\strace,\,\handler,\,\cstrace,\,\cex,\,\econt,\,{#2})} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\Break{\env}{\scont} \label{breakcont:break} \\ |
| &\FinallyBreak{\stmt}{\scont} \label{breakcont:finallybreak} |
| \end{align} |
| \caption{Break Continuations} |
| \label{figure:breakcont} |
| \end{eqfigure} |
| \end{figure} |
| |
| The break continuation Break, \ref{breakcont:break}, captures a statement continuation and the environment corresponding to a target label or a break statement. |
| The break continuation FinallyBreak, \ref{breakcont:finallybreak}, captures the statement body and the components necessary for the execution of an enclosing Finally statement. |
| They are added when a try/finally statement is executed. |
| |
| |
| \subsubsection{Switch Continuations} |
| \label{subsubsec:switch-continuations} |
| |
| Switch continuations, $\switchcont$, capture the steps to be executed when a continue to a preceding switch case statement is executed. |
| They capture the components needed for the execution of the case body statement. |
| The different switch continuations are shown in Figure~\ref{figure:switchconts}. |
| |
| \newcommand{\ContinueK}{\mathrm{SwitchContinueK}(\stmt,\,\env,\,\lbls,\,\clbls,\,\handler,\,\cstrace,\,\cex,\,\econt,\,\scont)} |
| \newcommand{\FinallyContinue}[2]{\mathrm{FinallyContinue}({#1},\,\env,\,\lbls,\,\clbls,\,\strace,\,\handler,\,\cstrace,\,\cex,\,\econt,\,{#2})} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\ContinueK \label{switchcont:continue} \\ |
| &\FinallyContinue{\stmt}{\scont} \label{switchcont:finallycontinue} |
| \end{align} |
| \caption{Switch Continuations} |
| \label{figure:switchconts} |
| \end{eqfigure} |
| \end{figure} |
| |
| The switch continuation SwitchContinue, \ref{switchcont:continue}, captures the statement body of a preceding switch case, targeted by some continue statement, and the components necessary for its execution. |
| The switch continuation FinallyContinue, \ref{switchcont:finallycontinue}, captures the statement body and the components necessary for the execution of an enclosing Finally statement. |
| They are added when a try/finally statement is executed. |
| |
| |
| \subsubsection{Exception Handlers} |
| \label{subsubsec:exception-handlers} |
| |
| The different exception handlers are shown in Figure~\ref{figure:handlers}. |
| \newcommand{\ThrowH}[2]{\mathrm{ThrowK}({#1},\,{#2})} |
| \newcommand{\CatchH}[1]{\mathrm{Catch}({#1},\,\env,\,\lbls,\,\clbls,\,\strace,\,\handler,\,\econt,\,\scont)} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\ThrowH{\val}{\strace} \label{handle:throw} \\ |
| &\CatchH{cs} \label{handle:catch} |
| \end{align} |
| \caption{Exception handlers} |
| \label{figure:handlers} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Event Loop Continuations} |
| |
| \newcommand{\StartNK}[3]{\mathrm{StartNK}({#1},\,{#2},\,{#3})} |
| \newcommand{\ResumeNK}[2]{\mathrm{ResumeNK}({#1},\,{#2})} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\StartNK{\stmt}{\env}{\econt}\\ |
| &\ResumeNK{\econt}{\val} |
| \end{align} |
| \caption{Event loop continuations} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \section{CESK Machine Transitions} |
| \label{sec:semantics} |
| |
| |
| \subsection{Expression Evaluation} |
| \label{subsec:expr-evaluation} |
| |
| |
| Expressions are evaluated by dispatching according to the expression component, $\expressionmeta$, in EvalConfiguration, Section~\ref{subsubsec:evalconfig}, and the list of expression component, $\exprs$, in EvalListConfiguration, Section~\ref{subsubsec:evallistconfig}. |
| |
| The CESK-transition function for EvalListConfiguration is shown in Figure~\ref{figure:evallist}. |
| The value corresponding to the evaluated expression is captured by the application continuation ValueA and eventually added to the list of values corresponding to the expressions. |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evallistconf{\expr :: \exprs}{\env}{\strace}{\cstrace}{\cex}{\acont}}% |
| {\evalconf{\expr}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\text{where $\econt = \ExpressionsK{\exprs}{\env}{\acont}$}} |
| \end{multlined}\\ |
| &\cesktrans% |
| {\evallistconf{[]}{\env}{\strace}{\cstrace}{\cex}{\acont}}% |
| {\acontconf{\acont}{[]}}\\ |
| &\cesktrans% |
| {\acontconf{\ValueA{\val}{\acont}}{\val s}}% |
| {\acontconf{\acont}{\val :: \val s}} |
| \end{align} |
| \caption{The CESK-transition function for EvalListConfiguration}\label{figure:evallist} |
| \label{subsec:eval-list-expressions} |
| \end{eqfigure} |
| \end{figure} |
| |
| %% |
| % Figure showing the CESK-transition function starting from EvalConfiguration for simple |
| % expressions. |
| %% |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\cesktranswhere% |
| {\evalconf{\IntLiteral{\integermeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\val}}% |
| {\text{where $\val = \mathrm{IntLiteral(\integermeta)} \in \dsemint$}} |
| \label{eval:int}\\ |
| &\cesktranswhere% |
| {\evalconf{\DoubleLiteral{\doublemeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\val}}% |
| {\text{where $\val = \mathrm{DoubleLiteral(\doublemeta)} \in \dsemdouble$}} |
| \label{eval:double}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\BoolLiteral{\true}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\val}}% |
| {\text{where $\val = \mathrm{BoolValue(\true)} = \true\in \dsembool$}} |
| \end{multlined} |
| \label{eval:true}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\BoolLiteral{\false}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\val}}% |
| {\text{where $\val = \mathrm{BoolValue(\false)} = \false\in \dsembool$}} |
| \end{multlined} |
| \label{eval:false}\\ |
| &\cesktranswhere% |
| {\evalconf{\StringLiteral{\stringmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\val}}% |
| {\text{where $\val = \mathrm{StringValue(\stringmeta)} \in \dsemstring$}} |
| \label{eval:string}\\ |
| &\cesktrans% |
| {\evalconf{\varmeta}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\deref{\env(\varmeta)}}} |
| \label{eval:varget}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\varmeta \synt{=} \expr}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expr}{\env}{\strace}{\cstrace}{\cex}{\econt'}} |
| {\econt' = \VarSetK{\variablemeta}{\env}{\ExceptionHandlers}{\econt}} |
| \end{multlined} |
| \label{eval:varset}\\ |
| &\cesktrans% |
| {\evalconf{\Not{\expressionmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\NotK{\econt}}} |
| \label{eval:not}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\AndExpression{\expressionmeta_0}{\expressionmeta_1}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta_0}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \AndK{\expressionmeta_1}{\env}{\econt}$}}% |
| \end{multlined} |
| \label{eval:and}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\OrExpression{\expressionmeta_0}{\expressionmeta_1}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta_0}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \OrK{\expressionmeta_1}{\env}{\econt}$}}% |
| \end{multlined} |
| \label{eval:or}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\ConditionalExpression{\expr}{\expri{1}}{\expri{2}}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expr}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where }\econt' = \ConditionalK{\expri{1}}{\expri{2}}{\env}{\econt}} |
| \end{multlined} |
| \label{eval:cond}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\Let{\varmeta}{\expri{1}}{\expri{2}}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expri{1}}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where }\econt' = \LetK{\varmeta}{\expri{2}}{\env}{\econt}} |
| \end{multlined} |
| \label{eval:let}\\ |
| &\begin{multlined} |
| \cesktranssplit% |
| {\evalconf{\StringConcatenation{\expressionmeta_1}{\expressionmeta_N}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evallistconf{\exprs}{\env}{\strace}{\cstrace}{\cex}{\StringConcatenationA}} |
| \end{multlined} |
| \label{eval:concat}\\ |
| &\cesktrans% |
| {\evalconf{\IsExpression{\expressionmeta}{\tt{T}}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\IsExpressionK}} |
| \label{eval:is}\\ |
| &\begin{multlined} |
| \cesktranssplit% |
| {\evalconf{\AsExpression{\expressionmeta}{\tt{T}}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\AsExpressionK}} |
| \end{multlined} |
| \label{eval:as}\\ |
| &\cesktrans% |
| {\evalconf{\this}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\deref{\env(\this)}}} |
| \label{eval:this}\\ |
| &\begin{multlined} |
| \cesktranssplit% |
| {\evalconf{\throw \expr}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expr}{\env}{\strace}{\cstrace}{\cex}{\ThrowH{(\throw \expr) :: \strace}{\handler}}} |
| \end{multlined} |
| \label{eval:throw}\\ |
| &\cesktrans% |
| {\evalconf{\rethrow}{\env}{\strace}{\strace'}{\cex}{\econt}}% |
| {\throwconf{\handler}{\cex}{\strace'}} |
| \label{eval:rethrow}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{F}{\env}{st}{cex}{cst}{\econt}}% |
| {\contconf{\econt}{\val}}% |
| {\begin{aligned} |
| \text{where } \val &= \funval{\formals}{\stmt}{\loc}\\ |
| F &\text{ is a function expression with formal parameters $\formals$ and body $\stmt$}\\ |
| \deref{\loc} &= \env \text{ after transtion} |
| \end{aligned}} |
| \end{multlined} |
| \end{align} |
| \caption{The CESK-transition function for EvalConfiguration: simple expressions} |
| \label{figure:expressions-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| %% |
| % Figure showing the CESK-transition function starting from ValuePassingConfiguration |
| % for simple expressions |
| %% |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranssplit% |
| {\contconf{\ExpressionsK{\exprs}{\env}{\acont}}{\val}}% |
| {\evallistconf{\exprs}{\env}{\strace}{\cstrace}{\cex}{\ValueA{\val}{\acont}}} |
| \end{multlined} |
| \label{econtconf:exprs}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\VarSetK{\idmeta}{\env}{\ExceptionHandlers}{\econt}}{\val}}% |
| {\contconf{\econt}{\val}}% |
| {\text{where $\deref{\env(\idmeta)} = \val$ after transition}} |
| \end{multlined} |
| \label{econtconf:varset}\\ |
| &\cesktrans% |
| {\contconf{\NotK{\econt}}{\true}}% |
| {\contconf{\econt}{\false}} |
| \label{econtconf:not-true}\\ |
| &\cesktrans% |
| {\contconf{\NotK{\econt}}{\false}}% |
| {\contconf{\econt}{\true}} |
| \label{econtconf:not-false}\\ |
| &\cesktrans% |
| {\contconf{\AndK{\expressionmeta}{\env}{\econt}}{\true}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt}} |
| \label{econtconf:and-true}\\ |
| &\cesktrans% |
| {\contconf{\AndK{\expressionmeta}{\env}{\econt}}{\false}}% |
| {\contconf{\econt}{\false}} |
| \label{econtconf:and-false}\\ |
| &\cesktrans% |
| {\contconf{\OrK{\expressionmeta}{\env}{\econt}}{\false}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt}} |
| \label{econtconf:or-false}\\ |
| &\cesktrans% |
| {\contconf{\OrK{\expressionmeta}{\env}{\econt}}{\true}}% |
| {\contconf{\econt}{\true}} |
| \label{econtconf:or-true}\\ |
| &\begin{multlined} |
| \cesktranssplit% |
| {\contconf{\ConditionalK{\expri{1}}{\expri{2}}{\env}{\econt}}{\true}}% |
| {\evalconf{\expri{1}}{\env}{\strace}{\cstrace}{\cex}{\econt}} |
| \end{multlined} |
| \label{econtconf:cond-true}\\ |
| &\begin{multlined} |
| \cesktranssplit% |
| {\contconf{\ConditionalK{\expri{1}}{\expri{2}}{\env}{\econt}}{\false}}% |
| {\evalconf{\expri{2}}{\env}{\strace}{\cstrace}{\cex}{\econt}} |
| \end{multlined} |
| \label{econtconf:cond-false}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\LetK{\expri{2}}{\env}{\varmeta}{\econt}}{\val}}% |
| {\evalconf{\expri{2}}{\env'}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\text{where $\env'=\ext{\env}{\varmeta}{\val}$}} |
| \end{multlined} |
| \label{econtconf:let}\\ |
| &\cesktranswhere% |
| {\contconf{\IsExpressionK}{\val}}% |
| {\contconf{\econt}{\true}}% |
| {\text{where $\val$ is $\tt{T}$}} |
| \label{econtconf:is-true}\\ |
| &\cesktranswhere% |
| {\contconf{\IsExpressionK}{\val}}% |
| {\contconf{\econt}{\false}}% |
| {\text{where $\val$ is not $\tt{T}$}} |
| \label{econtconf:is-false}\\ |
| &\cesktranswhere% |
| {\contconf{\AsExpressionK}{\val}}% |
| {\contconf{\econt}{\val}}% |
| {\text{where $\val$ is $\tt{T}$}} |
| \label{econtconf:as-true}\\ |
| &\cesktranswhere% |
| {\contconf{\AsExpressionK}{\val}}% |
| {\throwconf{\handler}{\AsExpression{\expressionmeta}{\tt{T}} :: \strace}{\synt{CastError}}}% |
| {\text{where $\val$ is not $\tt{T}$}} |
| \label{econtconf:as-false} |
| \end{align} |
| \caption{The CESK-transition function for ValuePassingConfiguration: simple expressions} |
| \label{figure:cont-config} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Basic Literal Evaluation} |
| \label{subsubsec:basic-literal-eval} |
| |
| \kernel{} literals are evaluated to a value $\val \in \dlitval$ in one step. |
| Transitions of the CESK machine for basic literals are presented in Figure~\ref{figure:expressions-evalconfigs}, rules \eqref{eval:int} - \eqref{eval:string}. |
| |
| |
| \subsubsection{Variable Assignment and Lookup} |
| \label{subsubsec:variable-assignment-and-lookup} |
| |
| A variable $\varmeta$ is accessed by reading the value stored at location $\env(\varmeta)$ in the store, \eqref{eval:varget}. |
| Assigning a value to a variable $\varmeta$ will modify the store, more specifically the value stored at location $\env(\varmeta)$. |
| The evaluation of this expression proceeds by evaluating the right-hand side expression, as shown in \eqref{eval:varset} and setting the location $\env(\varmeta)$ in the store to the value this expression evaluates to, as shown in \eqref{econtconf:varset}. |
| |
| |
| \subsubsection{Boolean Expressions} |
| \label{subsubsec:bool-expressions} |
| |
| The CESK-transition function for boolean expressions is show in Figure~\ref{figure:expressions-evalconfigs}, rules \eqref{eval:not} - \eqref{eval:cond}. |
| |
| \begin{itemize} |
| \item Not expression\\ |
| The target expression is evaluated, as shown in \eqref{eval:not} and proceed by dispatching on the value the expression evaluates to according to \eqref{econtconf:not-true} and \eqref{econtconf:not-false}. |
| |
| \item And expression\\ |
| The left-hand side expression is evaluated, according to \eqref{eval:and}. |
| We dispatch on the value the expression evaluates to. |
| If the expression evaluate to $\false$, according to \eqref{econtconf:and-false}, the value is immediately applied to the current expression continuation. |
| Otherwise, we proceed with the CESK-transition \eqref{econtconf:and-true}, by also evaluating the right-hand side. |
| |
| \item Or expression\\ |
| The left-hand side expression is evaluated, as shown in the CESK-transition \eqref{eval:or}. |
| We dispatch on the value the expression evaluates to. |
| If the expression evaluates to $\true$, according to \eqref{econtconf:or-true}, the value is immediately applied to the current expression continuation. |
| Otherwise, we proceed with the CESK-transition \eqref{econtconf:or-false}, by also evaluating the right-hand side. |
| |
| \item Conditional expression\\ |
| The condition expression is evaluated, as shown in the CESK-transition \eqref{eval:cond}. |
| We dispatch on the value the expression evaluates to. |
| If the expression evaluates to $\true$, the next configuration evaluates the first expression and is produced with the CESK-transition \eqref{econtconf:cond-true}. |
| Otherwise, the next configuration evaluates the second expression and is produced with the transition \eqref{econtconf:cond-false}. |
| |
| \end{itemize} |
| |
| |
| \subsubsection{Let} |
| |
| Let expressions in \kernel{} introduce a new variable, initialized to some value with an initializer expression, for the evaluation of the right-hand side let expression. |
| Let expressions are evaluated by first evaluating the initializer expression for the fresh variable as shown in the CESK-transition \eqref{eval:let}. |
| It proceeds by extending the environment for the evaluation of the right-hand side let expression and producing the next configuration for evaluation of the later with the CESK-transition \eqref{econtconf:let}. |
| |
| |
| \subsubsection{String Concatenation} |
| \label{subsubsec:string-concatenation} |
| |
| The function $\concat$ concatenates the strings from the given meta-list into a single value. |
| \begin{align*} |
| \concat : \mlist{\dsemstring} &\rightarrow \dsemstring\\ |
| \concat( s_1 :: \dots :: s_n :: []) &= s_1 \dots s_n |
| \end{align*} |
| The evaluation of concatenation expression proceeds by evaluating the target expressions in the specified order, as shown with the CESK-transition \eqref{eval:concat}. |
| Once all expressions have been evaluated the corresponding application is applied, as shown in \eqref{acontconf:concat}, which results with an expression continuation application to the resulting $\dsemstring$. |
| |
| |
| \subsubsection{This} |
| |
| For the evaluation of $\this$ expression we add a special variable declaration, $\this$. |
| In the body of instance methods or constructors, there is a binding in the corresponding environment from $\this$ variable declaration to a location that stores the corresponding value. |
| Evaluation of $\this$ expression resolves to that value in one step, as shown in \eqref{eval:this}. |
| |
| |
| \subsubsection{Type Test} |
| \label{subsubsec:type-test} |
| |
| Type test expressions evaluate to a boolean literal value, in more than one step. |
| The evaluation of this kind of expression proceeds by evaluating the target expression, as in CESK-transition \eqref{eval:is}. |
| When the target expression evaluates to a value $\val$ such that ``$\val $ is $\tt{T}$" holds, the value $true$ is applied to the expression continuation, $\econt$, as shown in \eqref{econtconf:is-true}, otherwise $\false$ is applied to $\econt$, as in \eqref{econtconf:is-false}. |
| |
| |
| \subsubsection{Type Cast} |
| \label{subsubsec:type-cast} |
| |
| Evaluation of type cast expression proceed to evaluation of the target expression to the corresponding value, as shown in \eqref{eval:as}. |
| When the target expression evaluates to a value $\val$ such that ``$\val $ is $\tt{T}$" holds, the value $\val$ is applied to the expression continuation as shown in \eqref{econtconf:as-true}. |
| Otherwise, the evaluation of the expression results with an error, as shown in \eqref{econtconf:as-false}. |
| |
| |
| \subsubsection{Function Expressions} |
| \label{subsubsec:function-expressions} |
| |
| \kernel{} supports encapsulating an executable unit of code with function expressions. |
| To support function expressions we introduce $fv = \funval{\formals}{\stmt_{body}}{\env} \in \dfunval$ as a value that has the function statement body, $\stmt_{body} \in \dstmt$, its list of formal parameters, $\formals \in \dformals$, and the environment, $\env \in \denv$ in scope of the function expression. |
| This ensures that there are no free variables in the body of $fv$. |
| |
| $fv \in \dfunval$ has only one property, $call$. |
| |
| %% |
| % Figure showing the CESK-transition function starting from ApplicationConfiguration. |
| %% |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktrans% |
| {\acontconf{\StringConcatenationA}{\vals}}% |
| {\contconf{\econt}{\concat(\vals)}} |
| \end{multlined} |
| \label{acontconf:concat}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\acontconf{\StaticInvA{\formals}{\stmt}{\strace}{\econt}}{\val{s}}}% |
| {\execconf{\stmt}{\env'}{[]}{[]}{\strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\parbox{10cm}{where $\scont = \ExitSK{\nnull}$, $\env' = \ext{\env_{empty}}{\formals}{\val{s}}$}} |
| \end{multlined} |
| \label{acontconf:staticinvoc} |
| \end{align} |
| \caption{The CESK-transition function for ApplicationConfiguration for static invocation} |
| \label{table:static-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Function Invocation} |
| \label{subsubsec:function-invoc} |
| |
| Function invocation occurs when a function expression (\ref{subsubsec:function-expressions}), instance method (\ref{subsubsec:instance-method-invoc}, \ref{subsubsec:direct-instance-method-invoc}, \ref{subsubsec:super-method-invoc}), a getter(\ref{subsubsec:property-extraction}), a setter (\ref{subsubsec:property-assignment}) or a constructor is invoked with new or with super and redirecting initializer (\ref{subsubsec:new-instance}). |
| |
| Instance method, getter or setter invocation proceed by evaluation of the receiver expression and binding its value to $\this$. |
| For the other invocations, $\this$ is not bound. |
| |
| Execution of function invocation proceeds immediately when the target function is marked as "sync". |
| \todo{Add text for generator sync and async function, and async function invocation.} |
| |
| The evaluation of the invocation proceeds by evaluating the actual argument list and binding the values of the evaluated argument list to the formal parameters of the function. |
| \kernel{} supports positional, positional optional and named arguments. |
| |
| An invocation expression for a \kernel{} function contains a list of expressions that represent the actual arguments for the invocation. |
| We construct a list of actual argument expressions containing the provided positional arguments and the provided named arguments. |
| We also add the constant default expressions for the optional positional and named parameters. |
| This is an implementation detail that allows us to evaluate all arguments for the invocation ignoring the distinction between provided or missing positional, optional and named arguments. |
| Note that the default values for the optional positional and named parameters are constants, hence their evaluation does not have side effects and they evaluate to a value in one step. |
| |
| After the evaluation of the argument expressions, and before binding the actual arguments to the formal parameters necessary checks ensure the actual arguments are valid. |
| |
| Let $(\val_1, \dots, \val_n, \{a_{n+1} : \val_{n+1}, \dots, a_{n+l} : \val_{n+l}\})$ be the list of values that correspond to the actual arguments expressions for the function invocation with $a_i$ names of actual named arguments. |
| The actual arguments are valid if: |
| \begin{itemize} |
| \item The number of positional actual arguments corresponds to the number of formal arguments for the function. |
| \item The actual names of named arguments $a_i$ correspond to named formal parameters. |
| \end{itemize} |
| |
| If any of the above mentioned statements doesn't hold, a "NoSuchMethodError" is thrown. |
| \todo{Elaborate how this error is constructed and passed to the current handler.} |
| \todo{Add text for type checking the parameters.} |
| |
| Otherwise, the statement body is then executed with the appropriate bindings. |
| The specific CESK-transitions for the different invocations are described in the appropriate sections below. |
| |
| %% |
| % Figure showing the CESK-transition function starting from EvalConfgiration for |
| % static property extraction and assignment, and static invocation |
| %% |
| \todo{zhivkag: Modify static method and getter invocation w.r.t. async semantics} |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\StaticGet{\membermeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\deref{\mainenv(\membermeta)}}}% |
| {\text{where $\membermeta$ is a static field and $\contains(\mainenv, \membermeta)$}} |
| \end{multlined} |
| \label{eval:staticget-var}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\StaticGet{\membermeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\nnull}}% |
| {\begin{aligned} |
| \text{where } &\membermeta \text{ is a static field without an initializer expression},\\ |
| ¬ \contains(\mainenv, \membermeta),\\ |
| &\deref{(\mainenv(\membermeta))} = \NullLiteral \text{ after transition} |
| \end{aligned}} |
| \end{multlined} |
| \label{eval:staticget-varnew-null}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\StaticGet{\membermeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\begin{aligned} |
| \text{where } &\membermeta \text{ is a static field with initializer expression $\expressionmeta$},\\ |
| ¬ \contains(\mainenv, \membermeta),\\ |
| &\econt' = \StaticGetK |
| \end{aligned}} |
| \end{multlined} |
| \label{eval:staticget-varnew}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\StaticGet{\membermeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\execconf{\stmt}{\env_{empty}}{[]}{[]}{\StaticGet{\membermeta} ::\strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } \membermeta &\text{is a getter with body $\stmt$}\\ |
| \scont &= \ExitSK{\nnull} |
| \end{aligned}} |
| \end{multlined} |
| \label{eval:staticget-getter}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\StaticGet{\membermeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\funval{\formals}{\stmt}{\loc}}}% |
| {\begin{aligned} |
| \text{where } \deref{\loc} &= \env_{empty} \text{ after transition}\\ |
| \membermeta &\text{ is a method tear-off with formal parameters $\formals$ and body $\stmt$} |
| \end{aligned}} |
| \end{multlined} |
| \label{eval:staticget-tearoff}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\StaticSet{\membermeta}{\expressionmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \StaticSetK$}} |
| \end{multlined} |
| \label{eval:staticset}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\StaticInvocation{\{\membermeta\}}{\expressionsmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evallistconf{\exprs}{\env}{\strace}{\cstrace}{\cex}{\acont'}}% |
| {\begin{aligned} |
| \text{where } \acont' &= \StaticInvA{\formals}{\stmt}{\strace'}{\econt},\\ |
| \strace' &= \StaticInvocation{\{\membermeta\}}{\expressionsmeta}::\strace,\\ |
| \membermeta &\text{ is a static method with formal parameters }\formals \text{ and body }\stmt |
| \end{aligned}} |
| \end{multlined} |
| \label{eval:staticinvoc} |
| \end{align} |
| \caption{The CESK-transition function for EvalConfiguration: static variable extraction and assignment, and sync static method invocation} |
| \label{table:static-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| %% |
| % Figure showing the CESK-transition function starting from ValuePassingConfiguration for |
| % static property extraction and assignment, and static invocation |
| %% |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\StaticGetK}{\val}}% |
| {\contconf{\econt}{\val}}% |
| {\begin{aligned} |
| \text{where }&\\ |
| \mainenv^{\synt{R}} &= \extend( \mainenv^{\synt{L}},\,\membermeta,\,\val) |
| \text{ after transition}\\ |
| \mainenv^{\synt{L}} &\text{ is the main environment in the starting configuration}\\ |
| \mainenv^{\synt{R}} &\text{ is the main environment in the resulting configuration} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:staticget}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\StaticSetK}{\val}}% |
| {\contconf{\econt}{\val}} |
| {\begin{aligned} |
| \text{where } |
| &\contains(\mainenv, \membermeta),\\ |
| &\deref{(\mainenv(\membermeta))} = \val \text{ after transition} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:staticset-var}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\StaticSetK}{\val}}% |
| {\contconf{\econt}{\val}} |
| {\begin{aligned} |
| \text{where } |
| ¬ \contains(\mainenv, \membermeta)\\ |
| &\mainenv^{\synt{R}} = \extend( \mainenv^{\synt{L}},\,\membermeta,\,\val)\\ |
| &\mainenv^{\synt{L}} \text{ is the main environment in the starting configuration}\\ |
| &\mainenv^{\synt{R}} \text{ is the main environment in the resulting configuration} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:staticset-var-new}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\StaticSetK}{\val}}% |
| {\execconf{\stmt}{\env}{[]}{[]}{\strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } &\membermeta \text{ is a static setter with formal parameter }\formal \text{ and body }\stmt\\ |
| &\scont = \ExitSK{\val},\\ |
| &\env = \ext{\env_{empty}}{\formal}{\val} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:staticset-setter} |
| \end{align} |
| \caption{The CESK-transition function for ValuePassingConfiguration: static variable extraction and assignment, and static method invocation} |
| \label{table:static-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Static and Library Fields} |
| \label{subsubsec:static-and-library-fields} |
| |
| In order to remember initialization and assignment of library variables and static variables, we introduce a global environment $\mainenv$ described in Section~\ref{subsec:main-env}. |
| The environment $\mainenv$ stores bindings for static and library fields to locations for all static and library fields allocated before the execution of the program. |
| Static and library variables are accessed with $\StaticGet{\membermeta}$. |
| The member $\membermeta$ can be a static or library field, a getter or a method. |
| When $\membermeta$ is a method, the expression $\StaticGet{\membermeta}$ is a method tear-off. |
| |
| \begin{itemize} |
| \item $\membermeta$ is a static or library field\\ |
| Let $\expressionmeta_{\membermeta}$ be $\membermeta$'s initializer expression. |
| \begin{itemize} |
| \item If $\membermeta$ is accessed for the first time during the program's execution, the evaluation of $\StaticGet{\membermeta}$ proceeds with evaluation of the initializer expression $\expressionmeta_{\membermeta}$. |
| \item If $\expressionmeta$ is $\nnull$, the location for $\membermeta$ is updated to store a $\nnull$ value, as shown in \eqref{eval:staticget-varnew-null}. |
| \item If $\expressionmeta$ is an expression, this expression is evaluated as shown in \eqref{eval:staticget-varnew}. |
| The expression will evaluate to some value $\val$ that will be applied to the corresponding continuations, as shown in \eqref{econtconf:staticget}: the location for the field $\membermeta$ is updated to store the value $\val$ and the continuation $\econt$ is applied to the value $\val$. |
| \item If the location for the member $\membermeta$ in the global environment $\env_{M}$ has been previously accessed or initialized and does not store the empty value $\emptyset$, the continuation $\econt$ is applied to the stored value, as shown in \eqref{eval:staticget-var}. |
| \end{itemize} |
| |
| \item $\membermeta$ is a static getter\\ |
| If $\membermeta$ is a static getter, the body of the getter is executed, as shown in \eqref{eval:staticget-getter}. |
| |
| \item $\membermeta$ is a static method tear-off\\ |
| If $\membermeta$ is a method with formal parameters $\formals$ and body $\stmt$, a new $\funval{\formals}{\stmt}{\loc}, \deref{\loc} = \env_{empty}$ is created and bound to the member in the global environment $\mainenv$, as shown in \eqref{eval:staticget-tearoff}. |
| The continuation $\econt$ is applied to this value. |
| |
| \end{itemize} |
| |
| Static and library variables are set with $\StaticSet{\membermeta}{\expressionmeta}$. |
| The target member can either be a static or library field, or it can be a static setter. For both cases, the right-hand side expression is evaluated first, as shown in \eqref{eval:staticset}. |
| |
| \begin{itemize} |
| \item $\membermeta$ is a static or library field\\ |
| The evaluation proceeds by updating the value stored at the corresponding location in the environment $\mainenv$, as shown in \eqref{econtconf:staticset-var}. |
| |
| \item $\membermeta$ is a static setter\\ |
| The evaluation proceeds by executing the statement body of the setter. |
| A statement continuation $\ExitSK{\val}$ is added that applies the given expression continuation $\econt$ to the value of the right-hand side expression. |
| The statement body is executed in an environment that has only the binding from the formal parameter of the static setter to the value of the right-hand side expression, as shown in \eqref{econtconf:staticset-setter}. |
| |
| \item Otherwise, $\membermeta$ is a static or library setter with body $\stmt$ and formal parameter $\formal$. |
| |
| \end{itemize} |
| |
| |
| \subsubsection{Static Invocation} |
| \label{subsubsec:static-invoc} |
| |
| Static invocation is supported with $\StaticInvocation{\{\membermeta\}}{\expressionsmeta}$ where $\membermeta$ is a function with statement body $\stmt$ and formal parameters $\formals$. |
| The evaluation of a static invocation proceeds by evaluating the arguments of the call, as shown in \eqref{eval:staticinvoc}. |
| After the evaluation of the actual arguments for the invocation, the corresponding application is applied to the resulting list of values, as shown in \eqref{acontconf:staticinvoc}. |
| In \eqref{acontconf:staticinvoc}, we apply the application continuation by creating a new environment for the execution of the body of the method by binding its formal parameters to the locations of the values for the actual arguments. |
| A statement continuation, $\ExitSK{\nnull}$ is added as next statement continuation to ensure that the execution of the body of the method returns correctly, when a return statement is not executed after the execution of the last statement of the body. |
| |
| %% |
| % Figure showing the CESK-transition function starting from |
| % ValuePassingConfiguration for instance property extraction and assignment. |
| %% |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\PropertyGet{\expressionmeta}{\idmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \PropertyGetK$}} |
| \end{multlined} |
| \label{eval:propertyget}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\DirectPropertyGet{\expressionmeta}{\membermeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \DPropertyGetK$}} |
| \end{multlined} |
| \label{eval:dpropertyget}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\PropertySet{\expressionmeta_0}{\idmeta}{\expressionmeta_1}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta_0}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \PropertySetK$}} |
| \end{multlined} |
| \label{eval:propertyset}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\DirectPropertySet{\expressionmeta_0}{\membermeta}{\expressionmeta_1}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta_0}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \DirectPropertySetK$}} |
| \end{multlined} |
| \label{eval:dpropertyset}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\SuperPropertyGet{\idmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{\val}}% |
| {\begin{aligned} |
| \text{where } \val &= \funval{\formals}{\stmt}{\loc}\\ |
| \deref{\loc} &= \env'\\ |
| \env' &= \ext{\env_{empty}}{\this}{\deref{(\env(\this))}},\\ |
| \membermeta &= \superclass(\deref{\env(\this)}).lookup(\idmeta),\\ |
| \membermeta &\text{ is a method tear-off with formal parameters $\formals$ and body $\stmt$} |
| \end{aligned}} |
| \end{multlined} |
| \label{eval:superpropertyget-tearoff}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\evalconf{\SuperPropertyGet{\idmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\execconf{\stmt}{\env'}{\lbls}{\clbls}{\SuperPropertyGet{\idmeta} :: \strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } \membermeta &= \superclass(\deref{\env(\this)}).lookup(\idmeta),\\ |
| \membermeta &\text{ is a getter method with body }\stmt,\\ |
| \env' &= \ext{\env_{empty}}{\this}{\deref{(\env(\this))}},\\ |
| \scont &= \ExitSK{\nnull} |
| \end{aligned}} |
| \end{multlined} |
| \label{eval:superpropertyget-getter}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\SuperPropertyGet{\idmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\contconf{\econt}{M(\deref{(\env(\this))})}}% |
| {\text{where $\membermeta = \superclass(\deref{\env(\this)}).lookup(\idmeta)$, $\membermeta$ is a implicit field getter}} |
| \end{multlined} |
| \label{eval:superpropertyget-field}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\SuperPropertySet{\idmeta}{\expressionmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \SuperPropertySetK$}} |
| \end{multlined} |
| \label{eval:superpropertyset} |
| \end{align} |
| \caption{The CESK-transition function for EvalConfiguration: instance property extraction and assignment} |
| \label{figure:instance-property-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| %% |
| % Figure showing the CESK-transition function starting from ValuePassingConfiguration for instance property extraction. |
| %% |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\PropertyGetK}{\val}}% |
| {\contconf{\econt}{\funval{\formals}{\stmt}{\loc}}} |
| {\begin{aligned} |
| \text{where } \membermeta &\text{ is a method with body $\stmt$ and formals $\formals$},\\ |
| \deref{\loc} &= \env \text{ after transition}\\ |
| \env &= \ext{\env_{empty}}{\this}{\val} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:propertyget-tearoff}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\PropertyGetK}{\val}}% |
| {\execconf{\stmt}{\env}{[]}{[]}{\PropertyGet{\val}{\idmeta} :: \strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } \membermeta&\text{ is a getter with body $\stmt$},\\ |
| \env &= \ext{\env_{empty}}{\this}{\val},\\ |
| \scont &= \ExitSK{\nnull} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:propertyget-getter}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\PropertyGetK}{\val}}% |
| {\contconf{\econt}{\text{\membermeta}(\val)}}% |
| {\begin{aligned} |
| \text{where } \membermeta &\text{ is an implicit getter for field $\idmeta$},\\ |
| \env &= \ext{\env_{empty}}{\this}{\val},\\ |
| \scont &= \ExitSK{\nnull} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:propertyget-field}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\PropertyGetK}{\val}}% |
| {\throwconf{\handler}{(\throw\text{ NoSuchMethod($\PropertyGet{\val}{\idmeta}$)}) :: \strace}{\text{NoSuchMethod}}}% |
| {\parbox{10cm}{where lookup of name $\idmeta$ was unsuccessful in class of value $\val$}} |
| \end{multlined} |
| \label{econtconf:propertyget-nosuchmethod}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\DPropertyGetK}{\val}}% |
| {\contconf{\econt}{\funval{\formals}{\stmt}{\loc}}}% |
| {\begin{aligned} |
| \text{where } \deref{\loc} = \env \text{ after transition}\\ |
| \membermeta &\text{ is a method with body $\stmt$ and formals $\formals$},\\ |
| \env &= \ext{\env_{empty}}{\this}{\val} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:dpropertyget-tearoff}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\DPropertyGetK}{\val}}% |
| {\execconf{\stmt}{\env}{[]}{[]}{\DirectPropertyGet{\val}{\membermeta} :: \strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } \membermeta &\text{ is getter with statement body $\stmt$},\\ |
| \env &= \ext{\env_{empty}}{\this}{\val},\\ |
| \scont &= \ExitSK{\nnull} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:dpropertyget-getter}\\ |
| &\begin{multlined} |
| \cesktranswhere% |
| {\contconf{\DPropertyGetK}{\val}}% |
| {\contconf{\econt}{\deref{\val[\membermeta]}}}% |
| {\text{where $\membermeta$ is a field }} |
| \end{multlined} |
| \label{econtconf:dpropertyget-field} |
| \end{align} |
| \caption{The CESK-transition function for ValuePassingConfiguration: instance property extraction} |
| \label{figure:econtconf:instance-property-extraction} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Property Extraction} |
| \label{subsubsec:property-extraction} |
| |
| \kernel{} allows access of a member as a property, which can be either getter access, which executes the getter, or method extraction, which converts a method into a closure, also known as tear-off. |
| Property extraction is supported with $\PropertyGet{\expr}{\idmeta}$. |
| The evaluation of this expression is shown in \eqref{eval:propertyget}. |
| After the evaluation of the receiver expression to a value $\val$, the property $\idmeta$ is looked up in methods, getters and implicit getters for the value $\val$. |
| Let $\membermeta$ be the instance member result of such successful lookup below and in \eqref{econtconf:propertyget-field}, \eqref{econtconf:propertyget-getter} and \eqref{econtconf:propertyget-tearoff}. |
| The evaluation of the expression proceeds as follow: |
| |
| \begin{itemize} |
| \item $\membermeta$ is a method tear-off\\ |
| When $\membermeta$ is a method tear-off, the evaluation of the property extraction expression proceeds as shown in \eqref{econtconf:propertyget-tearoff}. |
| The member is converted to a value $\val \in \dfunval$, capturing the method body, its formal parameters and an environment with a $\this$ binding to a location that stores the current instance value and the expression continuation $\econt$ is applied to it. |
| |
| \item $\membermeta$ is a getter\\ |
| When $\membermeta$ is a getter, the body of the getter is executed as shown in the CESK-transition function step \eqref{econtconf:propertyget-getter}. |
| The statement body is executed with an environment with a $\this$ binding to a location that stores the current instance value and no statement continuation. |
| A getter should always contain a reachable return statement. |
| |
| \item $\membermeta$ is an implicit getter for a field $\idmeta$\\ |
| When $\membermeta$ is an implicit getter for field $\idmeta$ it is immediately applied on the receiver expression. |
| Application of implicit getter on some instance value returns the value stored in the location this getter contains. |
| Afterwards the continuation expression is applied to the value, as shown in \eqref{econtconf:propertyget-field}. |
| |
| \end{itemize} |
| |
| If the lookup fails, a ``NoSuchMethod'' will be thrown, as shown in \eqref{econtconf:propertyget-nosuchmethod}. |
| |
| |
| \subsubsection{Direct Property Extraction} |
| \label{subsubsec:direct-property-extraction} |
| |
| In \kernel{} a property can be accessed without lookup, by direct reference to the member $\membermeta$. |
| This implies that the lookup step above is bypassed. |
| Similar to Section~\ref{subsubsec:property-extraction}, this expression can be either getter access, which executes the getter, or method extraction, which converts a method into a closure, also known as tear-off. |
| The evaluation proceeds as follows: |
| |
| \begin{itemize} |
| \item $\membermeta$ is an instance method\\ |
| When $\membermeta$ is an instance method the evaluation of the direct property extraction expression proceeds in the same way as in Section~\ref{subsubsec:property-extraction}. |
| The exact CESK-transition function for this case is shown in \eqref{econtconf:dpropertyget-tearoff}. |
| |
| \item $\membermeta$ is an instance getter\\ |
| When $\membermeta$ is an instance getter, the statement body of the getter is executed, as described in the previous section with the CESK-transition function shown in \eqref{econtconf:dpropertyget-getter}. |
| |
| \item $\membermeta$ is an instance field\\ |
| When $\membermeta$ is an instance field, the evaluation proceeds as shown in \eqref{econtconf:dpropertyget-field}. |
| |
| \end{itemize} |
| |
| %% |
| % Figure showing the CESK-transition function starting from |
| % ValuePassingConfiguration for instance property assignment. |
| %% |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\PropertySetK}{\val_0}}% |
| {\evalconf{\expressionmeta_1}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\text{where $\econt' = \PropertySetVK$}} |
| \end{multlined} |
| \label{econtconf:propertyset-val}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\PropertySetVK}{\val_1}}% |
| {\execconf{\stmt}{\env}{[]}{[]}{(\PropertySet{\val_0}{\idmeta}{\val_1}) :: \strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } \lookupMember(\class(\val_0),\,\idmeta) &= \text{Setter}(A, S),\\ |
| \env &= \ext{\env_{empty}}{\this :: \formal :: []}{\val_0 :: \val_1 :: []},\\ |
| \scont &= \ExitSK{\val_1}\\ |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:propertyset-setter}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\PropertySetVK}{\val}}% |
| {\contconf{\econt}{\val_1}}% |
| {\begin{aligned} |
| \text{where } \lookupMember(\class(\val_0),\,\idmeta) &= \text{Setter}(i \in \NN),\\ |
| \deref{(\getfield(\val_0,\, i))} &= \val \text{ after the transtion}\\ |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:propertyset-field}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\DirectPropertySetK}{\val_0}}% |
| {\evalconf{\expressionmeta_1}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\parbox{10cm}{where $\econt' = \DPropertySetVK$}} |
| \end{multlined} |
| \label{econtconf:dpropertyset-val}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\DPropertySetVK}{\val_1}} |
| {\execconf{\stmt}{\env}{\lbls}{\clbls}{(\DirectPropertySet{\val_0}{\membermeta}{\val_1}) :: \strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}} |
| {\begin{aligned} |
| \text{where } \membermeta &= \text{Setter}(\formal, \stmt),\\ |
| \env &= \ext{\env_{empty}}{\this :: \formal :: []}{\val_0 :: \val_1 :: []}\\ |
| \scont &= \ExitSK{\val_1} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:dpropertyset-setter}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\DPropertySetVK}{\val}}% |
| {\contconf{\econt}{\val}}% |
| {\begin{aligned} |
| \text{where } \membermeta &= \text{Setter}(i \in \NN),\\ |
| \deref{(\getfield(\val_0,\, i))} &= \val \text{ after the transtion}\\ |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:dpropertyset-field}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\SuperPropertySetK}{\val}} |
| {\execconf{\stmt}{\env'}{\lbls}{\clbls}{(\SuperPropertySet{\idmeta}{\val}) :: \strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}} |
| {\begin{aligned} |
| \text{where } c &= \superclass(\class(\deref{(\env(\this))}))\\ |
| \lookupMember(c,\,\idmeta) &= \text{Setter}(\formal, \stmt)\\ |
| \env' &= \ext{\env_{empty}}{\this :: \formal :: []}{\deref{(\env(\this))} :: \val :: []}\\ |
| \scont &= \ExitSK{\val} |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:superpropertyset-setter}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\contconf{\SuperPropertySetK}{\val}}% |
| {\contconf{\econt}{\val}}% |
| {\begin{aligned} |
| \text{where } c &= \superclass(\class(\deref{(\env(\this))}))\\ |
| \lookupMember(c,\,\idmeta) &= \text{Setter}(i \in \NN)\\ |
| \deref{(\getfield(\deref{(\env(\this))},\, i))} &= \val \text{ after the transtion}\\ |
| \end{aligned}} |
| \end{multlined} |
| \label{econtconf:superpropertyset-field} |
| \end{align} |
| \caption{The CESK-transition function for ValuePassingConfiguration: instance property assignment} |
| \label{figure:instance-property-assignment-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Property Assignment} |
| \label{subsubsec:property-assignment} |
| |
| An assignment in \kernel{} results with the invocation of a setter. |
| The evaluation of a property assignment proceeds as follows. |
| First, the left-hand side expression, i.e. the receiver expression, is evaluated as shown in \eqref{eval:propertyset}. |
| Afterwards, the right-hand side expression is evaluated, as shown in \eqref{econtconf:propertyset-val}. |
| After the evaluation of the receiver expression to a value $\val_0$ and the argument to value $\val_1$, the property $\idmeta$ is looked up in the properties for the value $\val_0$. |
| and implicit setters for the value $\val_0$. |
| Let $\membermeta$ be the result of such lookup. |
| The evaluation proceeds as follows: |
| |
| \begin{itemize} |
| \item $\membermeta$ is a setter invocation\\ |
| When $\membermeta$ is an invocation of a setter with body $\stmt$ and formal parameter $\formal$, the evaluation proceeds by executing the body in the environment which binds $\this$ to a location that contains $\val_0$ and the formal parameter $\formal$ to a location that contains $\val_1$. |
| This is shown in the CESK-transition \eqref{econtconf:propertyset-setter}. |
| Note that we add the special statement continuation $\ExitSK{\val_1}$, that will apply the value $\val_1$ to the current expression continuation. |
| |
| \item $\membermeta$ is a field\\ |
| When the lookup results with a field, the implicit setter for the field is invoked with the receiver value and the field value as shown in \eqref{econtconf:propertyset-field}. |
| The $\{\membermeta\}(\val_0, \val_1)$ is the implicit setter for the field $\membermeta$ which is a function in the domain $\dval \times \dval \rightarrow \dval$. |
| The value returned by the implicit function is $\val_1$. |
| |
| \end{itemize} |
| |
| |
| \subsubsection{Direct Property Assignment} |
| \label{subsubsec:direct-property-assignment} |
| |
| In \kernel{} a property can be set without lookup, by direct reference to the member of the instance. |
| This implies that the lookup step described in \ref{subsubsec:property-assignment} above is bypassed. |
| The evaluation of direct property assignment proceeds by evaluating the right-hand side expression, i.e. the receiver expression as shown in \eqref{eval:dpropertyset}. |
| Afterwards, the evaluation continues with the left-hand side expression as shown in \eqref{econtconf:dpropertyset-val}. |
| After evaluating the receiver expression to $\val_0$ and the argument expression to $\val_1$, depending on $\membermeta$, the evaluation continues as follows: |
| |
| \begin{itemize} |
| \item $\membermeta$ is an instance setter\\ |
| When $\membermeta$ is an instance setter with body $\stmt$ and formal parameter $\formal$, the evaluation of the expression proceeds with execution of the body with an environment binding $\this$ to a location containing $\val_0$ and the formal parameter $\formal$ to a location storing $\val_1$. |
| |
| \item $\membermeta$ is a field\\ |
| When $\membermeta$ is a field the value stored at location $\val_0[\membermeta]$ is modified to store value the argument expression evaluates to, $\val_1$, as shown in \eqref{econtconf:dpropertyset-field}. |
| |
| \end{itemize} |
| |
| |
| \subsubsection{Super Property Get} |
| \label{subsubsec:super-property-get} |
| |
| \kernel{} allows access of a superclass member as a property, which can be either getter access, which executes the getter, or method extraction, which converts a method into a closure. |
| Accessing a superclass member is accessed with the expression $\SuperPropertyGet{\idmeta}$ evaluated with the corresponding components: $\env$, $\strace$, $\handler$, $\cstrace$, $\cex$, $\econt$. |
| Let $\val = \deref{(\env(\this))}$, $C = \superclass(\val)$ and $\membermeta$ the result of looking up $\idmeta$ in $C$. |
| The evaluation of a super property extraction proceeds as follows: |
| |
| \begin{itemize} |
| \item $\membermeta$ is a method tear-off\\ |
| When $\membermeta$ is a method tear-off, the evaluation of super property extraction expression proceeds as shown in \eqref{eval:superpropertyget-tearoff}. |
| The member with body $\stmt$ and formal parameters $\formals$ is converted to a value $\val \in \dfunval$. |
| The value $\val$ captures the method body, its formal parameters and an environment with a $\this$ binding to a location that stores the current instance value and the expression continuation $\econt$ is applied to it. |
| |
| \item $\membermeta$ is an instance getter\\ |
| When $\membermeta$ is an instance getter, the statement body of the getter is executed. |
| The CESK-transition is shown in \eqref{eval:superpropertyget-getter}. |
| |
| \item $\membermeta$ is an instance field\\ |
| When $\membermeta$ is an instance field, the evaluation proceeds as shown in \eqref{eval:superpropertyget-field}. |
| |
| \end{itemize} |
| |
| |
| \subsubsection{Super Property Assignment} |
| \label{subsubsec:super-property-assignemnt} |
| |
| \kernel{} supports assignment of a super member with the expression $\SuperPropertySet{\idmeta}{\expressionmeta}$. |
| Let $\val' = \deref{(\env(\this))}$, $C = \superclass(\val')$ and $M$ the result of looking up $\idmeta$ in $C$. |
| The evaluation proceeds with evaluation of the right-hand side expression as shown in \eqref{eval:superpropertyset}. |
| After the evaluation of the argument expression to a value $\val$, depending on $\membermeta$, the evaluation continues as follows: |
| |
| \todo{regroup all property extraction together since text is similar} |
| \begin{itemize} |
| \item $\membermeta$ is an instance setter\\ |
| When $\membermeta$ is an invocation of a setter with body $\stmt$ and formal parameter $\formal$, the evaluation proceeds by executing the body in the environment which binds $\this$ to a location that contains $\deref{(\env(\this))}$ and the formal parameter $\formal$ to a location that contains $\val$. |
| This is shown in the CESK-transition \eqref{econtconf:superpropertyset-setter}. |
| Note that we add the special statement continuation $\ExitSK{\val_1}$, that will apply the value $\val$ to the current expression continuation. |
| |
| \item $\membermeta$ is a field\\ |
| When the lookup results with a field, the implicit setter for the field is invoked with the receiver value $\deref{(\env(\this))}$ and the field value $\val$, as shown in \eqref{econtconf:superpropertyset-field}. |
| |
| \end{itemize} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\InstanceMethodInvocation{\expressionmeta}{\idmeta}{\expressionsmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\econt' = \InstanceMethodK{\InstanceMethodInvocation{\expressionmeta}{\idmeta}{\expressionsmeta} :: \strace}} |
| \end{multlined} |
| \label{eval:instancemethod}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\DInstanceMethodInvocation{\expressionmeta}{\membermeta}{\expressionsmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evalconf{\expressionmeta}{\env}{\strace}{\cstrace}{\cex}{\econt'}}% |
| {\econt' = \DInstanceMethodK{\DInstanceMethodInvocation{\expressionmeta}{\membermeta}{\expressionsmeta} :: \strace}} |
| \end{multlined} |
| \label{eval:dinstancemethod}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\SuperMethodInvocation{\idmeta}{\expressionsmeta}}{\env}{\strace}{\cstrace}{\cex}{\econt}}% |
| {\evallistconf{\expressionsmeta}{\env}{\strace}{\cstrace}{\cex}{\acont}}% |
| {\acont = \SuperMethodA{\SuperMethodInvocation{\idmeta}{\expressionsmeta} :: \strace}} |
| \end{multlined} |
| \label{eval:superinstancemethod}\\ |
| &\begin{multlined} |
| \cesktranswheresplit% |
| {\evalconf{\new Q(\exprs)}{\env}{st}{cex}{cst}{\econt}}% |
| {\evallistconf{\exprs}{\env}{st}{cex}{cst}{\acont'}}% |
| {\acont' = \ConstructorA{Q}{\new Q(\exprs) :: \strace}{\econt}} |
| \end{multlined} |
| \label{eval:new} |
| \end{align} |
| \caption{The CESK-transition function for EvalConfiguration: instance method and constructor invocation} |
| \label{figure:instance-method-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\InstanceMethodK{\strace}}{\val}}% |
| {\evallistconf{\expressionsmeta}{\env}{\strace}{\cstrace}{\cex}{\acont'}}% |
| {\text{where $\acont' = \InstanceMethodA$}} |
| \end{multlined} |
| \label{econtconf:instancemethod}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\DInstanceMethodK{\strace}}{\val}}% |
| {\evallistconf{\expressionsmeta}{\env}{\strace}{\cstrace}{\cex}{\acont'}}% |
| {\text{where $\acont' = \DInstanceMethodA$}} |
| \end{multlined} |
| \label{econtconf:dinstancemethod} |
| \end{align} |
| \caption{The CESK-transition function for ValuePassingConfiguration: instance method and constructor invocation} |
| \label{figure:instance-method-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\InstanceMethodA}{\val{s}}}% |
| {\execconf{\stmt}{\env}{[]}{[]}{\strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } \membermeta &= class(\val).lookup(\idmeta)\text{ is an instance method with body $\stmt$ and formals $\formals$},\\ |
| \scont &= \ExitSK{\nnull},\\ |
| \env &= \ext{\env_{empty}}{\this :: \formals}{\val :: \val{s}} |
| \end{aligned}} |
| \end{multlined} |
| \label{acontconf:instancemethod}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\DInstanceMethodA}{\val{s}}}% |
| {\execconf{\stmt}{\env}{[]}{[]}{\strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } \stmt &\text{ is the statement body and $\formals$ are the formal parameters of the instace method $\membermeta$},\\ |
| \scont &= \ExitSK{\nnull},\\ |
| \env &= \ext{\env_{empty}}{\this :: \formals}{\val :: \val{s}} |
| \end{aligned}} |
| \end{multlined} |
| \label{acontconf:dinstancemethod}\\ |
| &\begin{multlined} |
| \cesktranswheresplit*% |
| {\contconf{\SuperMethodA{\strace}}{\val{s}}}% |
| {\execconf{\stmt}{\env'}{[]}{[]}{\strace}{\handler}{\cex,\,\cstrace}{\econt}{\scont}}% |
| {\begin{aligned} |
| \text{where } c &= \superclass(\class(\val))\\ |
| \membermeta &= \lookupMember(c,\,\idmeta)\text{ is an instance method with body $\stmt$ and formals $\formals$},\\ |
| \scont &= \ExitSK{\nnull},\\ |
| \env' &= \ext{\env_{empty}}{\this :: \formals}{\deref{(\env(\this))} :: \val{s}} \end{aligned}} |
| \end{multlined} |
| \label{acontconf:superinstancemethod} |
| \end{align} |
| \caption{The CESK-transition function for ApplicationConfigurations} |
| \label{figure:instance-method-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| \begin{figure}[Htp] |
| \begin{eqfigure} |
| \begin{align} |
| \cesktrans% |
| {\scontconf{\ExitSK{\val}}{\env}}% |
| {\contconf{\econt}{\val}} |
| \end{align} |
| \caption{The CESK-transition function for ForwardConfigurations} |
| \label{figure:instance-method-evalconfigs} |
| \end{eqfigure} |
| \end{figure} |
| |
| |
| \subsubsection{Instance Method Invocation} |
| \label{subsubsec:instance-method-invoc} |
| |
| Method invocation is supported with $\InstanceMethodInvocation{\expressionmeta}{\idmeta}{\expressionsmeta}$. |
| |
| The evaluation of instance method invocation proceeds with the evaluation of the left-hand side expression, i.e. the receiver expression as shown in \eqref{eval:instancemethod}. |
| As shown in the CESK-transition \eqref{econtconf:instancemethod}, the argument expressions evaluate to a list of values. |
| After the evaluation of the receiver expression to a value $\val$, we proceed with evaluation of the argument expressions. |
| |
| After the evaluation of the receiver expression to a value $\val$ and the argument expressions to $\vals$, the instance method $\idmeta$ is looked up in the instance methods for the value $\val$. |
| Let $\membermeta$ be the result of such lookup with statement body $\stmt$ and formal parameters $\formals$. |
| |
| The body $\stmt$ is then executed with an environment binding $\this$ to a location storing the instance value $\val$ and the formal parameters to fresh locations each storing the values in $\vals$. |
| The CESK-transition is shown in \eqref{acontconf:instancemethod}. |
| |
| We add $\ExitSK{\nnull}$ as next statement continuation. |
| When a $\return$ statement is missing in the statement body $\stmt$ of the instance method $\membermeta$, the statement continuation $\ExitSK{\val}$ ensures that the execution will proceed to the corresponding expression continuation, in this case with $\val = \nnull$. |
| |
| |
| \subsubsection{Direct Instance Method Invocation} |
| \label{subsubsec:direct-instance-method-invoc} |
| |
| Direct method invocation allows invocation of instance method by providing directly the member method to be invoked and bypass the lookup step described in Section~\ref{subsubsec:instance-method-invoc} above. |
| The evaluation of the direct instance method invocation proceeds with the evaluation of the left-hand side expression, i.e. the receiver expression as shown in \eqref{eval:dinstancemethod}. |
| After the evaluation of the receiver expression to a value $\val$, the evaluation proceeds with the evaluation of the argument expressions as shown in \eqref{acontconf:dinstancemethod}. |
| The argument expressions are evaluated to a list of values $\vals$. |
| The evaluation of the expression continues with the execution of the statement body in the environment that binds $\this$ to a location that stores the value $\val$ and the formal parameters $\formals$ to fresh locations storing values from $\vals$ accordingly. |
| The CESK-transition is shown in \eqref{acontconf:dinstancemethod}. |
| Similar to Section~\ref{subsubsec:instance-method-invoc}, $\ExitSK{\nnull}$ is added as next statement continuation. |
| |
| |
| \subsubsection{Super Method Invocation} |
| \label{subsubsec:super-method-invoc} |
| |
| Super method invocation is supported with $\SuperMethodInvocation{\idmeta}{\expressionsmeta}$. |
| We first evaluate the argument expressions, as shown in the CESK-transition \eqref{eval:superinstancemethod}. |
| After the evaluation of the argument expressions to list of values $\vals$ for the super method invocation, the evaluation continues with lookup for $\idmeta$ in the members of the value bound to $\this$ in the current environment. |
| Let $\val = \deref{(\env(\this))}$, $C = \superclass(\val)$ and $M$ the result of looking up $\idmeta$ in $C$. |
| Let $\stmt$ be the statement body and $\formals$ the formal parameters for $\membermeta$. |
| The statement $\stmt$ is executed in an environment binding $\formals$ to the locations containing the values in $\vals$ and $\this$ binding to location containing the same value bound to $\this$ in the current environment. |
| Similarly to Section~\ref{subsubsec:instance-method-invoc}, $\ExitSK{\val}$ is added as next statement continuation. |
| |
| |
| \subsubsection{New Instance Creation} |
| \label{subsubsec:new-instance} |
| |
| \kernel{} supports new instance creation with constructor invocation. |
| A constructor can be run with $\new$ expression or when it is a target of an initializer. |
| \kernel{} also supports redirecting constructors, which invoke a specified target constructor without modifying the newly allocated instance. |
| |
| A constructor has an associated class definition, an initializer list, $Izs$, with various kinds of initializers, formal parameters, $\formals$, and a statement body $\stmt$. |
| |
| We support the following kinds of initializers: |
| |
| \begin{itemize} |
| \item $\FieldInitializer{\expressionmeta}$ --- Field initializer for field $\field$ with expression $\expressionmeta$. |
| Field initializers modify the field of the newly allocated instance to store the value the expression evaluates to. |
| \item $\LocalInitializer{\expressionmeta}$ --- Local initializer for variable $\varmeta$ with expression $\expressionmeta$. |
| Local initializers extend the environment for the initializer list of the constructor with a binding of variable declaration $\varmeta$ to the value the expression evaluates to. |
| \item $\RedirectingInitializer{G}{\expressionsmeta}$ --- Redirecting initializer with target constructor $G$ and actual arguments for running the constructor $\expressionsmeta$. |
| Redirecting initializer appears last in the list of initializers of a constructor. |
| When the last initializer in the initializer list of a constructor is a redirecting initializer, we say the constructor is a redirecting constructor. |
| The redirecting constructor has an empty statement body. |
| When a redirecting constructor is run, only the initializer list of the constructor is executed. |
| Note that in other cases we first initialize instance fields in the immediately enclosing class that have initializer expressions before proceeding to execution of the initializer list. |
| Fields for the newly allocated instance from the immediately enclosing class are initialized only when a non-redirecting constructor is run. |
| This ensures that side effects from evaluating the actual arguments for the target constructor of the redirecting constructor occur before any side effects from initializing the fields in the immediately enclosing class. |
| \item $\SuperInitializer{G}{\expressionsmeta}$ --- Super initializer with target constructor $G$ and actual arguments for running the constructor $\expressionsmeta$. |
| |
