Statements.tex

\chapter{Statements\label{chap:Statements}}
Statements update storage elements and determine the flow of control in a subprogram.

\ExampleDef{Statements}
\listingref{Statements} shows some examples of statements.
\ASLListing{Examples of statements}{Statements}{\definitiontests/Statements.asl}

\ChapterOutline
\begin{itemize}
  \item \FormalRelationsRef{Statements} defines the formal relations used for statements;
  \item \secref{PassStatements} defines pass statements;
  \item \secref{AssignmentStatements} defines assignment statements;
  \item \secref{SetterAssignmentStatements} defines setter assignment statements;
  \item \secref{DeclarationStatements} defines declaration statements;
  \item \secref{DeclarationStatementsElidedParameter} defines declaration statements with an elided parameter;
  \item \secref{SequencingStatement} defines sequencing statements;
  \item \secref{CallStatements} defines call statements;
  \item \secref{ConditionalStatements} defines conditional statements;
  \item \secref{CaseStatements} defines case statements;
  \item \secref{AssertionStatements} defines assertion statements;
  \item \secref{WhileStatements} defines while statements;
  \item \secref{RepeatStatements} defines repeat statements;
  \item \secref{ForStatements} defines for-looping statements;
  \item \secref{ThrowStatements} defines throw statements;
  \item \secref{TryStatements} defines try statements;
  \item \secref{ReturnStatements} defines return statements;
  \item \secref{PrintStatements} defines print statements;
  \item \secref{UnreachableStatement} defines unreachable statements;
  \item \secref{PragmaStatements} defines pragma statements.
\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\FormalRelationsDef{Statements}
\paragraph{Syntax:} Statements are grammatically derived from $\Nstmt$.

\paragraph{Abstract Syntax:} Statements are derived in the abstract syntax from $\stmt$
and generated by $\buildstmt$.
\NotImportedToASLSpecYet{
\hypertarget{build-stmt}{}
The function
\[
\buildstmt(\overname{\parsenode{\Nstmt}}{\vparsednode}) \;\aslto\; \overname{\stmt}{\vastnode}
\]
transforms a statement parse node $\vparsednode$ into a statement AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION


\paragraph{Typing:} Statements are annotated by $\annotatestmt$.
\RenderRelation{annotate_stmt}

\paragraph{Semantics:} Statements are evaluated by $\evalstmt$.
\RenderRelation{eval_stmt}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Pass Statements\label{sec:PassStatements}}
\hypertarget{def-passstatementterm}{}

\ASLListing{A \texttt{pass} statement}{semantics-spass}{\semanticstests/SemanticsRule.SPass.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tpass \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_pass}


\ASTRuleDef{SPass}
\begin{mathpar}
\inferrule{}{
  \buildstmt(\overname{\Nstmt(\Tpass, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SPass}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SPass}
\ExampleDef{Typing a Pass Statement}
Annotating the \passstatementterm{} in \listingref{semantics-spass} does
not modify the \staticenvironmentterm{}.


\RenderProseAndFormally{annotate_stmt_SPass}
\CodeSubsection{\SPassBegin}{\SPassEnd}{../Typing.ml}

\subsection{Semantics}
\SemanticsRuleDef{SPass}
\ExampleDef{Evaluation of Pass Statements}
In \listingref{semantics-spass}, \texttt{pass;} does not modify the environment.


\RenderProseAndFormally{eval_stmt_SPass}
\CodeSubsection{\EvalSPassBegin}{\EvalSPassEnd}{../Interpreter.ml}

\hypertarget{def-assignmentstatementterm}{}
\section{Assignment Statements\label{sec:AssignmentStatements}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Nlexpr \parsesep \Teq \parsesep \Nexpr \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_assign}


\ASTRuleDef{SAssign}
\begin{mathpar}
\inferrule{}{
  \buildstmt(\overname{\Nstmt(\punnode{\Nlexpr}, \Teq, \punnode{\Nexpr}, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SAssign(\astof{\vlexpr}, \astof{\vexpr})}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SAssign}
\ExampleDef{Typing an Assignment Statement}
In \listingref{semantics-sassign}, the assignment \verb|x = 3;|
is well-typed.


\RenderProseAndFormally{annotate_stmt_SAssign}
\CodeSubsection{\SAssignBegin}{\SAssignEnd}{../Typing.ml}

\subsection{Semantics}
There are two rules for evaluating assignments:
\begin{itemize}
\item \SemanticsRuleRef{SAssignCall} handles assignments where the \rhsexpression{}
      is a \callexpressionterm{} and the left-hand-side expression is a tuple.
\item \SemanticsRuleRef{SAssign} handles all other assignments.
\end{itemize}

Although the sequential semantics of both types of statements is the same,
their concurrent semantics are different.
\SemanticsRuleRef{SAssignCall} generates a different execution graph ---
one where each value of the left-hand-side tuple depends on the \executiongraphterm{}
for the corresponding (that is, at the same position) value returned from the \callexpressionterm{}.
In contrast, the \executiongraphterm{} generated by \SemanticsRuleRef{SAssign}
creates dependencies between the entire \executiongraphterm{} for the evaluated right-hand-side
expression and the entire \executiongraphterm{} for the left-hand-side \executiongraphterm{}.

The rules for assignments first produce a value for the right-hand side expression
and then complete the update to the environment via an appropriate rule for evaluating the
\assignableexpression{} on the left-hand-side of the assignment.
The rules for updating the \assignableexpression{} handle variables, tuples, bitvectors, etc.

\SemanticsRuleDef{SAssignCall}
\ExampleDef{Evaluation of Multi-variable Assignment from Subprogram Calls}
In \listingref{assigncallsemantics}, given that the function call \texttt{f(1)} returns a triple of values ---
$\nvint(1)$, $\nvint(2)$, and $\nvint(3)$
(each with its own associated execution graph),
the statement \texttt{(a,b,-) = f(1)} assigns the value $\nvint(1)$ to the mutable variable \texttt{a},
$\nvint(2)$ to the mutable variable~\texttt{b}, and discards $\nvint(3)$.

\ASLListing{Assignment from a call expression.}{assigncallsemantics}{\semanticstests/SemanticsRule.SAssignCall.asl}


\RenderProseAndFormally{eval_stmt_SAssignCall}
\CodeSubsection{\EvalSAssignCallBegin}{\EvalSAssignCallEnd}{../Interpreter.ml}

\SemanticsRuleDef{SAssign}
\ExampleDef{Evaluation of Assignment Statements}
In \listingref{semantics-sassign},
\texttt{x = 3;} binds \texttt{x} to $\nvint(3)$ in the environment where \texttt{x} is bound to
$\nvint(42)$, and $\newenv$ is such that \texttt{x} is bound to $\nvint(3)$.
\ASLListing{Evaluating an assignment}{semantics-sassign}{\semanticstests/SemanticsRule.SAssign.asl}


\RenderProseAndFormally{eval_stmt_SAssign}
\CodeSubsection{\EvalSAssignBegin}{\EvalSAssignEnd}{../Interpreter.ml}

\SemanticsRuleDef{LexprIsVar}
\RenderRelation{lexpr_is_var}

In \ExampleRef{Evaluation of Multi-variable Assignment from Subprogram Calls},
the \assignableexpressions{} \verb|a|, \verb|b| are variables,
and \verb|-| is a discarded \assignableexpression{}.

\RenderProseAndFormally{lexpr_is_var}

\section{Setter Assignment Statements\label{sec:SetterAssignmentStatements}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \
   & \Ncall \parsesep \Nsetteraccess \parsesep \Teq \parsesep \Nexpr \parsesep \Tsemicolon &\\
|\ & \Ncall \parsesep \Nsetteraccess \parsesep \Nslices \parsesep \Teq \parsesep \Nexpr \parsesep \Tsemicolon &\\
|\ & \Ncall \parsesep \Tdot \parsesep \Tlbracket \parsesep \Clisttwo{{\Tidentifier}} \parsesep \Trbracket \parsesep \Teq \parsesep \Nexpr \parsesep \Tsemicolon &\\
\Nsetteraccess \derives \
   & \emptysentence &\\
|\ & \Tdot \parsesep \Tidentifier \parsesep \Nsetteraccess &
\end{flalign*}

\SyntacticSugarDef{SetterFieldAssignment}

If a setter is followed by a slice or field access, then the assignment to that bitslice is
implemented using the following Read-Modify-Write (RMW) behaviour:
\begin{itemize}
\item invoking the getter of the same name as the setter, with the same actual
      arguments as the setter invocation, excluding the right-hand side of the assignment;
\item performing the assignment to the bitslice or field of the result of the
      getter invocation; and
\item invoking the setter to assign the resulting value.
\end{itemize}
This is implemented by desugaring via \ASTRuleRef{DesugarSetter}.
%
See \ExampleRef{A Setter Call as a Read-Modify-Write}.

\ASTRuleDef{MakeSetter}
\NotImportedToASLSpecYet{
\hypertarget{def-makesetter}{}
The function
\[
\makesetter(
  \overname{\call}{\vcall} \aslsep
  \overname{\expr}{\varg}) \aslto \overname{\call}{\vcallp}
\]
constructs a setter call $\vcallp$ using a base call $\vcall$ and right-hand side $\varg$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule{}{
  \makesetter(\vcall, \varg) \aslto
    \overname{\left\{
      \begin{array}{rcl}
        \callname &:& \vcall.\callname,\\
        \callparams &:& \vcall.\callparams,\\
        \callargs &:& [\varg]\concat\vcall.\callargs,\\
        \callcalltype &:& \STSetter
      \end{array}
    \right\}}{\vcallp}
}
\end{mathpar}

\ASTRuleDef{DesugarSetter}
\NotImportedToASLSpecYet{
\hypertarget{def-desugarsetter}{}
The function
\[
\desugarsetter(
  \overname{\call}{\vcall} \aslsep
  \overname{\lhsaccess}{\vlhsaccess} \aslsep
  \overname{\expr}{\rhs}) \aslto \overname{\stmt}{\news}
\]
builds a statement $\news$ from an assignment of expression $\rhs$ to a setter invocation $\vcall.\callname$ with accesses given by $\vlhsaccess$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule[empty]{
  \vlhsaccess.\lhsaccessaccess = \emptylist \\
  \vlhsaccess.\lhsaccessslices = \emptylist \hva\\\\
  \makesetter(\vcall, \rhs) \aslto \vcallp
}{
  \desugarsetter(\vcall, \vlhsaccess, \rhs)
  \astarrow
  \SCall(\vcallp)
}
\end{mathpar}

\begin{mathpar}
\inferrule[non\_empty]{
  \vlhsaccess.\lhsaccessaccess \neq \emptylist \lor
  \vlhsaccess.\lhsaccessslices \neq \emptylist \hva\\\\
  \vx \in \Identifier \text{ is fresh} \hva\\\\
  \desugarlhsaccess(\vx, \vlhsaccess) \astarrow \lhs \\
  \vmodify \eqdef \SAssign(\lhs, \rhs) \\
  \readmodifywrite(\vcall, \vx, \vmodify) \astarrow \vcallp
}{
  \desugarsetter(\vcall, \vlhsaccess, \rhs)
  \astarrow
  \vcallp
}
\end{mathpar}

\ASTRuleDef{DesugarSetterSetfields}
\NotImportedToASLSpecYet{
\hypertarget{def-desugarsettersetfields}{}
The function
\[
\desugarsettersetfields(
  \overname{\call}{\vcall} \aslsep
  \overname{\KleeneStar{\Identifier}}{\vfields} \aslsep
  \overname{\expr}{\rhs}) \aslto \overname{\stmt}{\news}
\]
builds a statement $\news$ from an assignment of $\rhs$ to a setter invocation $\vcall.\callname$ with concatenated field accesses given by $\vfields$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule{
  \vx \in \Identifier \text{ is fresh} \hva\\\\
  \lhs \eqdef \LESetFields(\LEVar(\vx), \vfields) \\
  \vmodify \eqdef \SAssign(\lhs, \rhs) \\
  \readmodifywrite(\vcall, \vx, \vmodify) \astarrow \vcallp
}{
  \desugarsettersetfields(\vcall, \fields, \rhs)
  \astarrow
  \vcallp
}
\end{mathpar}

\ASTRuleDef{ReadModifyWrite}
\NotImportedToASLSpecYet{
\hypertarget{def-readmodifywrite}{}
The function
\[
\readmodifywrite(
  \overname{\call}{\vcall} \aslsep
  \overname{\Identifier}{\vx} \aslsep
  \overname{\stmt}{\vmodify}) \aslto \overname{\stmt}{\news}
\]
builds a sequence of statements to read from the getter invocation $\vcall.\callname$, modify the resulting value using $\vmodify$, and write it to a setter invocation $\vcall.\callname$.
} % END_OF_UNIMPORTED_RELATION

\ExampleDef{A Setter Call as a Read-Modify-Write}
\listingref{ReadModifyWriteSlice} shows how a setter call followed by a slice is
\desugared.
\ASLListing{A Setter followed by a Slice}{ReadModifyWriteSlice}{\syntaxtests/ASTRule.ReadModifyWriteSlice.asl}

\listingref{ReadModifyWriteField} shows how a setter call followed by a field access is
\desugared.
\ASLListing{A Setter followed by a Field Access}{ReadModifyWriteField}{\syntaxtests/ASTRule.ReadModifyWriteField.asl}

\begin{mathpar}
\inferrule{
  \setcalltype(\vcall, \STGetter) \aslto \vgetter \hva\\\\
  \vread \eqdef \SDecl(\LDKVar, \LDIVar(\vx), \none, \some{\ECall(\vgetter)}) \hva\\\\
  \makesetter(\vcall, \EVar(\vx)) \aslto \vsetter\\
  \news \eqdef \SSeq (\SSeq(\vread, \vmodify), \SCall(\vsetter))
}{
  \readmodifywrite(\vcall, \vx, \vmodify) \astarrow \news
}
\end{mathpar}

\ASTRuleDef{SetterAssign}
\begin{mathpar}
\inferrule[no\_slices]{
  \buildaccess(\vsetteraccess) \astarrow \vaccess \hva\\\\
  {
  \vlhsaccess \eqdef
    \left\{
      \begin{array}{rcl}
        \lhsaccessaccess &:& \vaccess,\\
        \lhsaccessslices &:& \emptylist
      \end{array}
    \right\}
  } \\
  \desugarsetter(\astof{\vcall}, \vlhsaccess, \astof{\vexpr}) \astarrow \vastnode
}{
  \buildstmt(\overname{\Nstmt(\punnode{\Ncall}, \namednode{\vsetteraccess}{\Nsetteraccess}, \Teq, \punnode{\Nexpr}, \Tsemicolon
  )}{\vparsednode})
  \astarrow \vastnode
}
\end{mathpar}

\begin{mathpar}
\inferrule[slices]{
  \buildaccess(\vsetteraccess) \astarrow \vaccess \hva\\\\
  {
  \vlhsaccess \eqdef
    \left\{
      \begin{array}{rcl}
        \lhsaccessaccess &:& \vaccess,\\
        \lhsaccessslices &:& \astof{\vslices}
      \end{array}
    \right\}
  } \\
  \desugarsetter(\astof{\vcall}, \vlhsaccess, \astof{\vexpr}) \astarrow \vastnode
}{
  {
    \begin{array}{r}
      \buildstmt(\overname{\Nstmt(\punnode{\Ncall}, \namednode{\vsetteraccess}{\Nsetteraccess}, \punnode{\Nslices}, \Teq, \punnode{\Nexpr}, \Tsemicolon
      )}{\vparsednode})
      \astarrow \\ \vastnode
    \end{array}
  }
}
\end{mathpar}

\begin{mathpar}
\inferrule[setfields]{
  \buildclist[\buildidentity](\vfields) \astarrow \vfieldasts \\
  \desugarsettersetfields(\astof{\vcall}, \vfieldasts, \astof{\vexpr}) \astarrow \vastnode
}{
  \buildstmt(\overname{\Nstmt(\punnode{\Ncall}, \Tdot,
    \Tlbracket, \namednode{\vfields}{\Clisttwo{\Tidentifier}}, \Trbracket, \Teq, \punnode{\Nexpr}, \Tsemicolon
  )}{\vparsednode})
  \astarrow \vastnode
}
\end{mathpar}

\subsection{Typing and semantics}
As given by applying the relevant rules to the desugared AST.

\hypertarget{def-declarationstatementterm}{}
\section{Declaration Statements\label{sec:DeclarationStatements}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Nlocaldeclkeyword \parsesep \Ndeclitem \parsesep \option{\Nasty} \parsesep \Teq \parsesep \Nexpr \parsesep \Tsemicolon &\\
|\ & \Tvar \parsesep \Ndeclitem \parsesep \Nasty \parsesep \Tsemicolon &\\
|\ & \Tvar \parsesep \Clisttwo{\Tidentifier} \parsesep \Nasty \parsesep \Tsemicolon &\\
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_decl}

\ASTRuleDef{SDecl}
\begin{mathpar}
\inferrule[let\_constant]{
  {
    \begin{array}{l}
  \vparsednode =\\ \Nstmt(\Nlocaldeclkeyword, \Ndeclitem, \namednode{\vt}{\option{\Nasty}}, \Teq, \punnode{\Nexpr}, \Tsemicolon)\\
  \end{array}
  }\hva\\
  \buildoption[\buildasty](\vt) \astarrow \astversion{\vt}\\
  \vastnode \eqdef \SDecl(\astof{\vlocaldeclkeyword}, \astof{\vdeclitem}, \astversion{\vt}, \some{\astof{\vexpr}})
}{
  \buildstmt(\vparsednode) \astarrow \vastnode
}
\end{mathpar}

\begin{mathpar}
\inferrule[uninit\_var]{}{
  {
  \begin{array}{r}
    \buildstmt(\overname{\Nstmt(\Tvar, \Ndeclitem, \punnode{\Nasty}, \Tsemicolon)}{\vparsednode})
    \astarrow \\
    \overname{\SDecl(\LDKVar, \astof{\vdeclitem}, \astof{\vasty}, \none)}{\vastnode}
  \end{array}
  }
}
\end{mathpar}

\begin{mathpar}
\inferrule[multi\_var]{
  \buildclist[\buildidentity](\vids) \astarrow \astversion{\vids}\\
  \buildasty(\vt) \astarrow \astversion{\vt} \hva\\
  \vstmts \eqdef [\vx\in\astversion{\vids}: \SDecl(\LDKVar, \vx, \astversion{\vt}, \none)]\\
  \stmtfromlist(\vstmts) \astarrow \vastnode
}{
  \buildstmt(\overname{\Nstmt(\Tvar, \namednode{\vids}{\Clisttwo{\Tidentifier}}, \namednode{\vt}{\Nasty}, \Tsemicolon)}{\vparsednode})
  \astarrow
  \vastnode
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SDecl}
\ExampleDef{Typing Declaration Statements}
\listingref{typing-sdecl} shows well-typed declaration statements.
\ASLListing{Typing declaration statements}{typing-sdecl}{\typingtests/TypingRule.SDecl.asl}

The specifications in \listingref{typing-sdecl-bad1} ill-typed,
since local constant storage elements are not allowed.
\ASLListing{A (illegal) local constant declaration}{typing-sdecl-bad1}{\typingtests/TypingRule.SDecl.bad1.asl}

The specification in \listingref{typing-sdecl-bad2} is ill-typed,
since immutable local storage elements require an initializing expression.
\ASLListing{An uninitialized immutable local storage declaration}{typing-sdecl-bad2}{\typingtests/TypingRule.SDecl.bad2.asl}


\RenderProseAndFormally{annotate_stmt_SDecl}
\CodeSubsection{\SDeclegin}{\SDeclEnd}{../Typing.ml}

\TypingRuleDef{AnnotateLocalDeclTypeAnnot}
\RenderRelation{annotate_local_decl_type_annot}

See \ExampleRef{Typing Declaration Statements}.


\RenderProseAndFormally{annotate_local_decl_type_annot}

\TypingRuleDef{InheritIntegerConstraints}
\RenderRelation{inherit_integer_constraints}

\listingref{typing-pendingconstrained} shows examples of pending-constrained
integer types.

\ExampleDef{Pending-constrained integer type vs. unconstrained integer type}
\listingref{pending-constrained-unconstrained} corresponds to the \typingerrorterm{}
in the \CaseName{int} below.
\ASLListing{An ill-typed pending-constrained integer type}{pending-constrained-unconstrained}
{\typingtests/TypingRule.InheritIntegerConstraints.unconstrained.bad.asl}


\RenderProseAndFormally{inherit_integer_constraints}

\TypingRuleDef{CheckNoPrecisionLoss}
\RenderRelation{check_no_precision_loss}

\ExampleDef{Rejected Declaration Because of Precision Loss}
In \listingref{typing-imprecisetype}, the statement \verb|var b = a * a;|
corresponds to the \typingerrorterm{} raised in the \CaseName{Well-Constrained}
below.
The type of the right-hand-side (\texttt{a * a}) is imprecise because the multiplication of two
constant types would result in more than $\maxconstraintsize$ elements, see
\TypingRuleRef{ApplyBinopTypes}.
\ASLListing{Type-checking a declaration with an imprecise type}{typing-imprecisetype}{\typingtests/TypingRule.CheckNoPrecisionLoss.asl}


\RenderProseAndFormally{check_no_precision_loss}
\CodeSubsection{\CheckNoPrecisionLossBegin}{\CheckNoPreciisonLossEnd}{../Typing.ml}

\TypingRuleDef{CheckCanBeInitializedWith}
\RenderRelation{check_can_be_initialized_with}

See \ExampleRef{Type-satisfaction Examples}.


\RenderProseAndFormally{check_can_be_initialized_with}


\subsection{Semantics}
\SemanticsRuleDef{SDecl}
Notice that \TypingRuleRef{SDecl} ensures that a typed \declarationstatementterm{}
has an initializing expression.
% The implementation still handles the case where there is no initializing expression,
% for cases where type-checking is skipped.

\ExampleDef{Declaration With an Initializing Value}
In \listingref{semantics-sdeclsome},
\texttt{let x = 3;} binds \texttt{x} to $\nvint(3)$ in the empty environment.
\ASLListing{Evaluating a declaration with a given initial value}{semantics-sdeclsome}{\semanticstests/SemanticsRule.SDeclSome.asl}

\ExampleDef{Declaration Without an Initializing Value}
In \listingref{semantics-sdeclnone},
\texttt{var x : integer;} binds \texttt{x} in $\env$ to the base value of \texttt{integer}.
\ASLListing{Evaluating a declaration without a given initial value}{semantics-sdeclnone}{\semanticstests/SemanticsRule.SDeclNone.asl}


\RenderProseAndFormally{eval_stmt_SDecl}
\CodeSubsection{\EvalSDeclBegin}{\EvalSDeclEnd}{../Interpreter.ml}

\section{Declaration Statements with an Elided Parameter\label{sec:DeclarationStatementsElidedParameter}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \
   & \Nlocaldeclkeyword \parsesep \Ndeclitem \parsesep \Nasty \parsesep \Teq \\
   & \wrappedline\ \Nelidedparamcall \parsesep \Tsemicolon &\\
\end{flalign*}

\begin{flalign*}
\Nelidedparamcall \derives \
     & \Tidentifier \parsesep \Tlbrace \parsesep \Trbrace &\\
  |\ & \Tidentifier \parsesep \Tlbrace \parsesep \Trbrace \parsesep \PlistZero{\Nexpr} &\\
  |\ & \Tidentifier \parsesep \Tlbrace \parsesep \Tcomma \parsesep \ClistOne{\Nexpr} \parsesep \Trbrace &\\
  |\ & \Tidentifier \parsesep \Tlbrace \parsesep \Tcomma \parsesep \ClistOne{\Nexpr} \parsesep \Trbrace \parsesep \PlistZero{\Nexpr}&
\end{flalign*}

\SyntacticSugarDef{ParameterElision}
In a call to a parameterized subprogram, a parameter can be elided,
if it can be inferred from the left-hand-side type annotation,
as detailed by \ASTRuleRef{ElidedParamCall} (See also \secref{ParameterElision}).

\ASTRuleDef{ElidedParamCall}
\hypertarget{build-elided-param-call}{}
The function $\buildelidedparamcall$ builds a $\call$ from a parsed $\Nelidedparamcall$.

\begin{mathpar}
\inferrule{
  \buildcall(\Ncall(\Tidentifier(\id), \Tlpar, \Trpar))
  \astarrow \vastnode
}{
  \buildelidedparamcall(\Nelidedparamcall (\Tidentifier(\id), \Tlbrace, \Trbrace))
  \astarrow \vastnode
}
\end{mathpar}

\begin{mathpar}
\inferrule{
  \vparsednode = \Nelidedparamcall(\Tidentifier(\id), \Tlbrace, \Trbrace, \namednode{\vargs}{\PlistZero{\Nexpr}})\\
  \buildcall(\Ncall(\Tidentifier(\id), \vargs))
  \astarrow \vastnode
}{
  \buildelidedparamcall(\vparsednode) \astarrow \vastnode
}
\end{mathpar}

\begin{mathpar}
\inferrule{
  \vparsednode = \Nelidedparamcall(\Tidentifier(\id), \Tlbrace, \Tcomma, \namednode{\vparams}{\ClistOne{\Nexpr}}, \Trbrace)\\
  \buildcall(\Ncall(\Tidentifier(\id), \Tlbrace, \vparams, \Trbrace))
  \astarrow \vastnode
}{
  \buildelidedparamcall(\vparsednode) \astarrow \vastnode
}
\end{mathpar}

\begin{mathpar}
\inferrule{
  {
  \vparsednode = \Nelidedparamcall\left(
    \begin{array}{l}
    \Tidentifier(\id), \Tlbrace, \Tcomma, \namednode{\vparams}{\ClistOne{\Nexpr}}, \Trbrace, \\
    \wrappedline\ \namednode{\vargs}{\PlistZero{\Nexpr}}
    \end{array}
    \right)
  }\hva\\
  \buildcall(\Ncall(\Tidentifier(\id), \Tlbrace, \vparams, \Trbrace, \vargs))
  \astarrow \vastnode
}{
  \buildelidedparamcall(\vparsednode) \astarrow \vastnode
}
\end{mathpar}

\ASTRuleDef{DesugarElidedParameter}
\NotImportedToASLSpecYet{
\hypertarget{def-desugarelidedparameter}{}
The function
\[
\desugarelidedparameter(
  \overname{\ty}{\vt} \aslsep
  \overname{\call}{\vcall})
\aslto
\overname{\Option{\expr}}{\vexpr}
\cup\ \overname{\TBuildError}{\ParseErrorConfig}
\]
builds an expression $\vexpr$ from an assignment of the call $\vcall$ to the left-hand side with type annotation $\vt$, where the call has an elided parameter.
Otherwise, the result is a parse error.
} % END_OF_UNIMPORTED_RELATION


\ExampleDef{Desugaring Parameter Elision Based on Declared Type Annotation}
\listingref{DesugarElidedParameter} shows examples of how parameters can be elided
if they can be copied from the type annotation in declaration statements.
\ASLListing{Desugaring parameter elision based on declared type annotation}{DesugarElidedParameter}{\syntaxtests/ASTRule.DesugarElidedParameter.asl}

\begin{mathpar}
\inferrule{
  \becheck(\vt = \TBits(\Ignore, \Ignore), \ParseError) \typearrow \True \;\terminateas \ParseErrorConfig \\
  \vt \reverseeqdef \TBits(\ve, \Ignore) \\
  \vcallp \eqdef \vcall[\callparams\mapsto [\ve] \concat \vcall.\callparams ]
}{
  \desugarelidedparameter(\ldk, \ldi, \vt, \vcall)
  \astarrow
  \some{\ECall(\vcallp)}
}
\end{mathpar}

\ASTRuleDef{ElidedParamDecl}
\begin{mathpar}
\inferrule{
  \buildelidedparamcall (\vcall) \astarrow \astversion{\vcall} \\
  \desugarelidedparameter(\astof{\vasty}, \astversion{\vcall}) \astarrow \vexpr
}{
  {
    \begin{array}{r}
    \buildstmt\left(
      \Nstmt\left(
        \begin{array}{l}
          \punnode{\Nlocaldeclkeyword}, \\
          \wrappedline\ \punnode{\Ndeclitem}, \punnode{\Nasty}, \Teq, \\
          \wrappedline\ \namednode{\vcall}{\Nelidedparamcall}, \Tsemicolon
        \end{array}
      \right)
    \right) \astarrow \\ \overname{\SDecl(\astof{\vlocaldeclkeyword}, \astof{\vdeclitem}, \some{\vasty}, \vexpr)}{\vastnode}
    \end{array}
  }
}
\end{mathpar}

\subsection{Typing and semantics}
As given by the applying the relevant rules to the desugared AST (see \secref{DeclarationStatements}).

\section{Sequencing Statements\label{sec:SequencingStatement}}
\hypertarget{def-sequencestatementterm}{}

\ASLListing{A sequence of statements}{semantics-sseq}{\semanticstests/SemanticsRule.SSeq.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmtlist \derives \ & \ListOne{\Nstmt} &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_seq}


\ASTRuleDef{StmtList}
\NotImportedToASLSpecYet{
\hypertarget{build-stmtlist}{}
The function
\[
  \buildstmtlist(\overname{\parsenode{\Nstmtlist}}{\vparsednode}) \;\aslto\; \overname{\stmt}{\vastnode}
\]
transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule{
  \buildlist[\Nstmt](\vstmts) \astarrow \vstmtlist\\
  \stmtfromlist(\vstmtlist) \astarrow \vastnode
}{
  \buildstmtlist(\Nstmtlist(\namednode{\vstmts}{\ListOne{\Nstmt}})) \astarrow \vastnode
}
\end{mathpar}

\ASTRuleDef{StmtFromList}
\NotImportedToASLSpecYet{
\hypertarget{def-stmtfromlist}{}
The function
\[
\stmtfromlist(\overname{\KleeneStar{\stmt}}{\vstmts}) \aslto \overname{\stmt}{\news}
\]
builds a statement $\news$ from a possibly-empty list of statements $\vstmts$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule[empty]{
}{
  \stmtfromlist(\overname{\emptylist}{\vstmts}) \astarrow \overname{\SPass}{\news}
}
\hva\and
\inferrule[non\_empty]{
  \stmtfromlist(\vstmtsone) \astarrow \vsone\\
  \sequencestmts(\vs, \vsone) \astarrow \news
}{
  \stmtfromlist(\overname{[\vs] \concat \vstmtsone}{\vstmts}) \astarrow \news
}
\end{mathpar}

\ASTRuleDef{SequenceStmts}
\NotImportedToASLSpecYet{
\hypertarget{def-sequencestmts}{}
The function
\[
\sequencestmts(\overname{\stmt}{\vsone}, \overname{\stmt}{\vstwo}) \aslto \overname{\stmt}{\news}
\]
Combines the statement $\vsone$ with $\vstwo$ into the statement $\news$, while filtering away
instances of $\SPass$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule[s1\_spass]{}{
  \sequencestmts(\overname{\SPass}{\vsone}, \vstwo) \astarrow \overname{\vstwo}{\news}
}
\hva\and
\inferrule[s2\_spass]{
  \vsone \neq \SPass
}{
  \sequencestmts(\vsone, \overname{\SPass}{\vstwo}) \astarrow \overname{\vsone}{\news}
}
\hva\and
\inferrule[no\_spass]{
  \vsone \neq \SPass\\
  \vstwo \neq \SPass
}{
  \sequencestmts(\vsone, \vstwo) \astarrow \overname{\SSeq(\vsone, \vstwo)}{\news}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SSeq}
\ExampleDef{Typing Sequencing Statements}
In \listingref{semantics-sseq}, the statement \verb|let x=3;| is
annotated first in the \staticenvironmentterm{} where the \localstaticenvironmentterm{} is empty.
Then, the statement \verb|let y = x + 1;|
is annotated in the \staticenvironmentterm{} where
\verb|x| has been declared and associated with the type \verb|integer{3}|,
and also recorded to be equivalent to $\LInt(3)$ (in the $\exprequiv$ map).


\RenderProseAndFormally{annotate_stmt_SSeq}
\CodeSubsection{\SSeqBegin}{\SSeqEnd}{../Typing.ml}

\subsection{Semantics}
\SemanticsRuleDef{SSeq}
\ExampleDef{Evaluation of Sequencing Statements}
In \listingref{semantics-sseq},
the evaluation of \texttt{let x = 3; let y = x + 1} first evaluates \texttt{let x = 3} and only then
evaluates \texttt{let y = x + 1}.


\RenderProseAndFormally{eval_stmt_SSeq}
\CodeSubsection{\EvalSSeqBegin}{\EvalSSeqEnd}{../Interpreter.ml}

\section{Call Statements\label{sec:CallStatements}}
\hypertarget{def-callstatementterm}{}
Call statements are used to invoke procedures and setters.

\ASLListing{Call Statements}{scall}{\semanticstests/SemanticsRule.SCall.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Ncall \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_call}

\ASTRuleDef{SCall}
\begin{mathpar}
\inferrule{
  \buildcall(\vcall) \astarrow \astversion{\vcall} \\
  \setcalltype(\astversion{\vcall}) \aslto \vcallp
}{
  \buildstmt(
  \overname{\Nstmt(\namednode{\vcall}{\Ncall}, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SCall(\vcallp)}{\vastnode}
}
\end{mathpar}

\ASTRuleDef{SetCallType}
\hypertarget{def-setcalltype}{}
In \ASTRuleRef{Call}, $\STFunction$ is inserted as a default call type for any parsed $\call$.
The function
\[
  \setcalltype(\overname{\call}{\vcall} \aslsep \overname{\subprogramtype}{\calltype}) \aslto \overname{\call}{\vcallp}
\]
changes the call type of $\vcall$ to $\calltype$.

\begin{mathpar}
\inferrule{}{
  \setcalltype(\vcall, \calltype) \aslto
  \overname{\vcall[\callcalltype\mapsto\calltype]}{\vcallp}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SCall}
In \listingref{scall}, the call statement \verb|catenate_into_g{4, 3}(x, y, TRUE);|
is well-typed.

\ExampleDef{Ill-defined Call to a Function}
In \listingref{scall-bad}, the call statement \verb|zero();| is ill-typed,
since call statements are only allowed for procedures, not functions.

\ASLListing{An ill-defined call statement}{scall-bad}{\typingtests/TypingRule.SCall.bad.asl}


\RenderProseAndFormally{annotate_stmt_SCall}
\CodeSubsection{\SCallBegin}{\SCallEnd}{../Typing.ml}


\subsection{Semantics}
\SemanticsRuleDef{SCall}
\ExampleDef{Evaluation of Call Statements}
In \listingref{scall}, the call statement \verb|catenate_into_g{4, 3}(x, y, TRUE);|
assigns \verb|'1101 111'| to the global variable \verb|g|.


\RenderProseAndFormally{eval_stmt_SCall}
\CodeSubsection{\EvalSCallBegin}{\EvalSCallEnd}{../Interpreter.ml}


\hypertarget{def-conditionalstatementterm}{}
\section{Conditional Statements\label{sec:ConditionalStatements}}

A conditional statement evaluates its \texttt{then} statement list if the
condition expression evaluates to $\True$. If the condition expression
evaluates to $\False$ each \texttt{elsif} condition expression is evaluated
sequentially until an \texttt{elsif} condition expression evaluates to $\True$;
the conditional statement evaluates the corresponding \texttt{elsif}
statement list. If no \texttt{elsif} condition expression evaluates to $\True$, the
conditional statement evaluates the \texttt{else} statement list.

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tif \parsesep \Nexpr \parsesep \Tthen \parsesep \Nstmtlist \parsesep \Nselse \parsesep \Tend \parsesep \Tsemicolon &\\
\Nselse \derives\ & \Telseif \parsesep \Nexpr \parsesep \Tthen \parsesep \Nstmtlist \parsesep \Nselse &\\
        |\ & \Telse \parsesep \Nstmtlist &\\
        |\ & \emptysentence &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_cond}


\ASTRuleDef{SCond}
\begin{mathpar}
\inferrule{}{
  {
    \begin{array}{r}
  \buildstmt(\overname{\Nstmt(\Tif, \punnode{\Nexpr}, \Tthen, \punnode{\Nstmtlist}, \punnode{\Nselse}, \Tend, \Tsemicolon)}{\vparsednode})
  \astarrow \\
  \overname{\SCond(\astof{\vexpr}, \astof{\vstmtlist}, \astof{\velse})}{\vastnode}
    \end{array}
  }
}
\end{mathpar}

\ASTRuleDef{SElse}
\NotImportedToASLSpecYet{
\hypertarget{build-selse}{}
The function
\[
  \buildselse(\overname{\parsenode{\Nselse}}{\vparsednode}) \;\aslto\; \overname{\stmt}{\vastnode}
\]
transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION

\begin{mathpar}
\inferrule[elseif]{}{
  {
    \begin{array}{r}
  \buildselse(\Nselse(\Telseif, \Nexpr, \Tthen, \Nstmtlist, \Nselse)) \astarrow \\
  \overname{\SCond(\astof{\vexpr}, \astof{\vstmtlist}, \astof{\vselse})}{\vastnode}
    \end{array}
  }
}
\end{mathpar}

\begin{mathpar}
\inferrule[pass]{}{
  \buildselse(\Nselse(\emptysentence)) \astarrow \overname{\SPass}{\vastnode}
}
\end{mathpar}

\begin{mathpar}
\inferrule[else]{}{
  \buildselse(\Nselse(\Telse, \punnode{\Nstmtlist})) \astarrow \overname{\astof{\vstmtlist}}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SCond}
The specifications in \listingref{semantics-scond},
\listingref{semantics-scond2},
\listingref{semantics-scond3}, and
\listingref{semantics-scond4} are all well-typed.

\ExampleDef{Typing Conditional Statements with Two Bitvector Types}
The specification in \listingref{SCond} is well-typed
and shows examples of how \bitvectortypesterm{} either \typesatisfyterm{}
the return type or do not \typesatisfyterm{} the return type and require
an \atcexpressionterm{}.
\ASLListing{Typing conditional statements with two bitvector types}{SCond}{\typingtests/TypingRule.SCond.asl}


\RenderProseAndFormally{annotate_stmt_SCond}
\CodeSubsection{\SCondBegin}{\SCondEnd}{../Typing.ml}


\subsection{Semantics}
\SemanticsRuleDef{SCond}
\ExampleDef{Conditional Statements}
The specification in \listingref{semantics-scond} does not result in any Assertion Error.
\ASLListing{Evaluating a conditional statement}{semantics-scond}{\semanticstests/SemanticsRule.SCond.asl}

The specification in \listingref{semantics-scond2}
does not result in any error.
\ASLListing{Evaluating a condition statement with \texttt{elsif}}{semantics-scond2}{\semanticstests/SemanticsRule.SCond2.asl}

The specification in \listingref{semantics-scond3}
results in an Assertion Error.
\ASLListing{Evaluating a condition statement that results in an Assertion Error}{semantics-scond3}{\semanticstests/SemanticsRule.SCond3.asl}

The specification in \listingref{semantics-scond4} does not result in any error.
\ASLListing{Evaluating a condition statement with only a \texttt{then} branch}{semantics-scond4}{\semanticstests/SemanticsRule.SCond4.asl}


\RenderProseAndFormally{eval_stmt_SCond}
\CodeSubsection{\EvalSCondBegin}{\EvalSCondEnd}{../Interpreter.ml}

\hypertarget{def-casestatementterm}{}
\section{Case Statements\label{sec:CaseStatements}}
Case statements allow executing different statements, based on which
condition an expression satisfies.

\listingref{case-discriminant} shows an example of a \casestatementterm{}
and the output to a console when it is evaluated.

\ASLListing{A side-effecting case discriminant}{case-discriminant}{\definitiontests/CaseStatement.discriminant.asl}
% CONSOLE_BEGIN aslref \definitiontests/CaseStatement.discriminant.asl
\begin{Verbatim}[fontsize=\footnotesize, frame=single]
num_tests: 0
selected case x=51
\end{Verbatim}
% CONSOLE_END
\listingref{case-discriminant} shows an example of a \casestatementterm{}
and the output to a console when it is evaluated.
%
\listingref{CaseStatement.where} shows an example of a \casestatementterm{}
with a \texttt{where} guard expression.

\hypertarget{def-casediscriminantterm}{}
\hypertarget{def-casealternativeterm}{}
\hypertarget{def-otherwisecaseterm}{}
The expression following the \Tcase\ keyword is called the \emph{\casediscriminantterm}.
The list following the \Tof\ keyword consists of \emph{\casealternativesterm},
optionally ending with an \emph{\otherwisecaseterm}, which follows the \Totherwise\ keyword.

Case statements obey the following requirements:

\RequirementDef{CaseDiscriminant} The \casediscriminantterm\ of a \texttt{case}
statement should be evaluated only once each time the case statement is evaluated.
%
\listingref{case-discriminant} demonstrates how the \casediscriminantterm{}
is evaluated only once.

\RequirementDef{CaseAlternatives} The \casealternativesterm\ are examined
one after another, in the order they are listed.
If any of the patterns match the \casediscriminantterm{} (and the guard
expression is true, if present) then this \casealternativeterm{} is considered selected,
its statement list is executed, and the \texttt{case} statement ends without examining any further
\casealternativesterm.
%
\listingref{case-discriminant} demonstrates how only one \casealternativeterm{} is selected
for execution.

\RequirementDef{CaseDiscriminantTesting} Testing the \casediscriminantterm{} against a \\
pattern list
follows the semantics of pattern matching defined in \chapref{PatternMatching}.
It is not a static error if it can be statically determined that none of the patterns in a
\casealternativeterm\ can match the discriminant.
%
\listingref{case-discriminant} exemplifies a \casestatementterm{} with pattern matching.

\RequirementDef{CaseOtherwise} If no \casealternativeterm\ is selected, and there is an
\otherwisecaseterm\, the \otherwisecaseterm\ is executed.
%
\listingref{case-otherwise} demonstrates how the \otherwisecaseterm{} is evaluated.

\ASLListing{Executing the \texttt{otherwise} case alternative}{case-otherwise}{\definitiontests/CaseStatement.otherwise.asl}
% CONSOLE_BEGIN aslref \definitiontests/CaseStatement.otherwise.asl
\begin{Verbatim}[fontsize=\footnotesize, frame=single]
num_tests: 0
selected otherwise
\end{Verbatim}
% CONSOLE_END

\RequirementDef{CaseNoOtherwiseError} If no \casealternativeterm\ is selected,
and there is no \otherwisecaseterm, it is a \dynamicerrorterm{}.
%
\listingref{case-no-otherwise} shows a specification that, when evaluated,
yields a \dynamicerrorterm{}.

\ASLListing{A case statement with no \texttt{otherwise} case}{case-no-otherwise}{\definitiontests/CaseStatement.no_otherwise.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tcase \parsesep \Nexpr \parsesep \Tof \parsesep \Ncasealtlist \parsesep \Tend \parsesep \Tsemicolon &\\
|\ & \Tcase \parsesep \Nexpr \parsesep \Tof \parsesep \Ncasealtlist \parsesep \Totherwise \parsesep \Tarrow &\\
   & \wrappedline\ \Nstmtlist \parsesep \Tend \parsesep \Tsemicolon &\\
\Ncasealtlist \derives \ & \ClistOne{\Ncasealt} \parsesep &\\
\Ncasealt \derives \ & \Twhen \parsesep \Npatternlist \parsesep \option{\Twhere \parsesep \Nexpr} \parsesep \Tarrow \parsesep \Nstmtlist &\\
\end{flalign*}

\listingref{CaseStatement-bad} shows an example of an erroneous case statement
where a \casealternativeterm{} is missing a statement.
\ASLListing{Invalid case statement syntax}{CaseStatement-bad}{\syntaxtests/CaseStatement.bad.asl}

\subsection{Abstract Syntax}

\SyntacticSugarDef{CaseStatement}
Case statements are considered \\ \syntacticsugar{}.
That is, there is no explicit representation for \texttt{case} statements
as they are represented in AST via a \conditionalstatementterm.
Case statements are \desugared{} by \ASTRuleRef{DesugarCaseStmt}.

\ExampleDef{Case Statement Desugaring}
\listingref{ast-case1} shows an example of how a \texttt{case} statement can be transformed into a corresponding
compound condition statement.
\ASLListing{Transforming a case statement with a variable as the case discriminant}{ast-case1}{\syntaxtests/ASTRule.Desugar_SCase1.asl}

\listingref{ast-case2} shows an example of how a \texttt{case} statement can be transformed into
a statement that does not contain any \text{case} statement.
By storing the \casediscriminantterm\ in a variable and by adding
an \unreachablestatementterm{}, the transformation ensures that a \dynamicerrorterm{} occurs when no
\casealternativeterm\ is selected.
\ASLListing{Transforming a case statement with a non-variable as the case discriminant
and no otherwise case}{ast-case2}{\syntaxtests/ASTRule.Desugar_SCase2.asl}

The untyped AST contains non-terminals for \casealternativesterm, which exist
only as a data type used by $\desugarcasestmt$ and do not later appear in the untyped
AST:

\RenderType[remove_hypertargets]{case_alt}

\ASTRuleDef{SCase}
To satisfy \RequirementRef{CaseNoOtherwiseError}, when no \otherwisecaseterm\ exists,\linebreak[2]
$\SUnreachable$ is used instead:
\begin{mathpar}
\inferrule[no\_otherwise]{
  \buildlist[\buildcasealt](\vcasealtlist) \astarrow \vcasealtlistast\\
  \buildexpr(\vediscriminant) \astarrow \astversion{\vediscriminant}\hva\\
  {
  \desugarcasestmt\left(
  \begin{array}{l}
    \astversion{\vediscriminant},\\
    \vcasealtlistast,\\
    \SUnreachable
  \end{array}
    \right) \astarrow
  \vastnode
  }
}{
  {
  \buildstmt\left(\overname{
    \Nstmt\left(
      \begin{array}{l}
        \Tcase, \namednode{\vediscriminant}{\Nexpr}, \Tof, \\
        \wrappedline\ \namednode{\vcasealtlist}{\Ncasealtlist}, \\
        \wrappedline\ \Tend, \Tsemicolon
      \end{array}
    \right)
    }{\vparsednode}\right)
  \astarrow
  \vastnode
  }
}
\end{mathpar}

\begin{mathpar}
\inferrule[otherwise]{
  \buildlist[\buildcasealt](\vcasealtlist) \astarrow \vcasealtlistast\\
  \buildexpr(\vediscriminant) \astarrow \astversion{\vediscriminant}\hva\\
  \buildstmtlist(\votherwise) \astarrow \astversion{\votherwise}\\
  {
  \desugarcasestmt\left(
  \begin{array}{l}
    \astversion{\vediscriminant},\\
    \vcasealtlistast,\\
    \astversion{\votherwise}
  \end{array}
    \right) \astarrow
  \vastnode
  }
}{
  {
  \buildstmt\left(\overname{
    \Nstmt\left(
      \begin{array}{l}
        \Tcase, \namednode{\vediscriminant}{\Nexpr}, \Tof, \\
        \wrappedline\ \namednode{\vcasealtlist}{\Ncasealtlist}, \\
        \wrappedline\ \Totherwise, \Tarrow, \\
        \wrappedline\ \namednode{\votherwise}{\Nstmtlist}, \\
        \wrappedline\ \Tend, \Tsemicolon
      \end{array}
    \right)
    }{\vparsednode}\right)
  \astarrow
  \vastnode
  }
}
\end{mathpar}

\ASTRuleDef{CaseAltList}
\NotImportedToASLSpecYet{
\hypertarget{build-casealtlist}{}
The function
\[
\buildcasealtlist(\overname{\parsenode{\Ncasealtlist}}{\vparsednode}) \;\aslto\; \overname{\KleenePlus{\casealt}}{\vastnode}
\]
transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION

\begin{mathpar}
\inferrule{
  \buildclist[\buildcasealt](\vcases) \typearrow \vastnode
}{
  \buildcasealtlist(\overname{\Ncasealtlist(\vcases : \ClistOne{\Ncasealt})}{\vparsednode}) \astarrow \vastnode
}
\end{mathpar}

\ASTRuleDef{CaseAlt}
\NotImportedToASLSpecYet{
\hypertarget{build-casealt}{}
The function
\[
\buildcasealt(\overname{\parsenode{\Ncasealt}}{\vparsednode}) \;\aslto\; \overname{\casealt}{\vastnode}
\]
transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION

\begin{mathpar}
\inferrule{
  \buildoption[\buildexpr](\vwhereopt) \astarrow \vwhereast
}{
  {
    \begin{array}{r}
  \buildcasealt\left(\overname{\Ncasealt\left(
    \begin{array}{l}
    \Twhen, \punnode{\Npatternlist}, \\
    \wrappedline\ \namednode{\vwhereopt}{\option{\Twhere, \Nexpr}}, \Tarrow, \\
    \wrappedline\ \namednode{\vstmts}{\Nstmtlist}
    \end{array}
    \right)}{\vparsednode}\right)
  \astarrow \\
  \overname{\casealt(\CasePattern: \astof{\vpatternlist}, \CaseWhere: \vwhereast, \CaseStmt: \astof{\vstmtlist})}{\vastnode}
    \end{array}
  }
}
\end{mathpar}

\ASTRuleDef{DesugarCaseStmt}
\NotImportedToASLSpecYet{
\hypertarget{def-desugarcasestmt}{}
The relation
\[
\desugarcasestmt(
  \overname{\expr}{\vezero},
  \overname{\KleeneStar{\casealt}}{\vcases},
  \overname{\stmt}{\votherwise}) \;\aslrel\; \overname{\stmt}{\news}
\]
transforms a \casediscriminantterm\ $\vezero$, a list of \casealternativesterm\ $\vcases$,
and a statement $\votherwise$ into a statement $\news$.
} % END_OF_UNIMPORTED_RELATION

\begin{mathpar}
\inferrule[var]{
  \astlabel(\vezero) = \EVar\\
  \casestocond(\vezero, \vcases, \votherwise) \typearrow \news
}{
  \desugarcasestmt(\vezero, \vcases, \votherwise) \astarrow \news
}
\end{mathpar}

To satisfy \RequirementRef{CaseDiscriminant}, the transformation assigns the
\casediscriminantterm\ to a temporary variable, which is then used in a
compound conditional statement (see \listingref{ast-case2} for an example):
\begin{mathpar}
\inferrule[non\_var]{
  \astlabel(\vezero) \neq \EVar\\
  \vx \in \Identifier \text{ is fresh}\hva\\
  \vdeclx \reverseeqdef \SDecl(\LDKLet, \LDIVar(\vx), \none, \some{\vezero})\\
  \casestocond(\EVar(\vx), \vcases, \votherwise) \typearrow \vscond
}{
  \desugarcasestmt(\vezero, \vcases, \votherwise) \astarrow \overname{\SSeq(\vdeclx, \vscond)}{\news}
}
\end{mathpar}
\CodeSubsection{\DesugarCaseStmtBegin}{\DesugarCaseStmtEnd}{../desugar.ml}

\ASTRuleDef{CasesToCond}
\NotImportedToASLSpecYet{
\hypertarget{def-casestocond}{}
The function
\[
\casestocond(
  \overname{\expr}{\ve} \aslsep
  \overname{\KleeneStar{\casealt}}{\vcases} \aslsep
  \overname{\stmt}{\votherwise})
\;\aslrel\; \overname{\stmt}{\news}
\]
transforms an expression $\ve$, a list of \texttt{case} alternatives $\vcases$,
and a statement $\votherwise$
into a statement $\news$.
} % END_OF_UNIMPORTED_RELATION

\begin{mathpar}
\inferrule[last]{
  \casetocond(\ve, \vcase, \votherwise) \astarrow \news
}{
  \casestocond(\ve, \overname{[\vcase]}{\vcases}, \votherwise) \astarrow \news
}
\end{mathpar}

\begin{mathpar}
\inferrule[not\_last]{
  \vcasesone \neq \emptylist\\
  \casestocond(\ve, \vcasesone) \typearrow \vsone\\
  \casetocond(\ve, \vcase, \vsone) \typearrow \news
}{
  \casestocond(\ve, \overname{[\vcase] \concat \vcasesone}{\vcases}, \votherwise) \astarrow \news
}
\end{mathpar}
\CodeSubsection{\CasesToCondBegin}{\CasesToCondEnd}{../desugar.ml}

\ASTRuleDef{CaseToCond}
\NotImportedToASLSpecYet{
\hypertarget{def-casetocond}{}
The function
\[
\casetocond(\overname{\expr}{\vezero} \aslsep \overname{\casealt}{\vcase} \aslsep \overname{\stmt}{\vtail})
\;\aslrel\; \overname{\stmt}{\news}
\]
transforms an expression $\vezero$ (the condition used for a \texttt{case} statement),
a single \texttt{case} alternative $\vcase$, and a statement $\vtail$, which represents
a list of \texttt{case} alternatives already converted to conditionals, into a condition statement $\news$.
} % END_OF_UNIMPORTED_RELATION

\begin{mathpar}
\inferrule{
  \vcase \reverseeqdef \{ \CasePattern : \vpattern, \CaseWhere : \vwhere, \CaseStmt : \vstmt \}\\
  \vepattern \eqdef \EPattern(\vezero, \vpattern)\hva\\
  {
  \vcond \eqdef \ifthenelseop[V]{\vwhere = \some{\vewhere}}{\EBinop(\BAND, \vepattern, \vewhere)}{\vepattern}
  }
}{
  \casetocond(\vezero, \vcase, \vtail) \astarrow \overname{\SCond(\vcond, \vstmt, \vtail)}{\news}
}
\end{mathpar}
\CodeSubsection{\CaseToCondBegin}{\CaseToCondEnd}{../desugar.ml}

\subsection{Typing}
Since case statements are transformed into other statements,
they do not require type system rules.


\subsection{Semantics}
Since case statements are transformed into other statements,
they do not appear in the typed AST and thus are not associated with a semantics.

In \listingref{CaseStatement.where} the expression \verb|a| will be evaluated twice.
\ASLListing{Evaluating case alternative sub-expressions}{CaseStatement.where}{\definitiontests/CaseStatement.where.asl}

\hypertarget{def-assertionstatementterm}{}
\section{Assertion Statements\label{sec:AssertionStatements}}
Assertion statements are used to check that certain conditions are satisfied.
They take a single \booleantypeterm{} operand, which we refer to as the
\emph{condition}. If the condition is \False, the statement fails with a
\dynamicerrorterm{} (\errorcodeterm{} $\DynamicAssertionFailure$).

\listingref{AssertionStatement} shows a possible use of
\assertionstatementterm{} to check the inputs to a function
(also known as a \emph{precondition})
and ensure the output satisfies expectations (also known as a \emph{postcondition}).
%
The first call to \verb|checked_8bit_add| succeeds, whereas the second call fails the
\assertionstatementterm{} \verb|assert a + b < 256;|

\ASLListing{Example of using \texttt{assert} statements}{AssertionStatement}{\definitiontests/AssertionStatement.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tassert \parsesep \Nexpr \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_assert}


\ASTRuleDef{SAssert}
\begin{mathpar}
\inferrule{}{
  \buildstmt(\overname{\Nstmt(\Tassert, \Nexpr, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SAssert(\astof{\vexpr})}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SAssert}
\ExampleDef{Type Assertion Statements}
The specifications in \listingref{semantics-sasertok} and \listingref{semantics-sassertno}
are well-typed.

The assertion statements in \listingref{assert-ill-typed} are ill-typed,
since the expression needs to be both of a \booleantypeterm{} and \readonlyterm{}.
\ASLListing{Ill-typed assertion statements}{assert-ill-typed}{\typingtests/TypingRule.SAssert.bad.asl}


\RenderProseAndFormally{annotate_stmt_SAssert}
\CodeSubsection{\SAssertBegin}{\SAssertEnd}{../Typing.ml}


\subsection{Semantics}
\SemanticsRuleDef{SAssert}
\ExampleDef{Evaluation of Assertions: Success}
In \listingref{semantics-sasertok},
\texttt{assert (42 != 3);} ensures that \texttt{3} is not equal to \texttt{42}.
\ASLListing{Evaluating an assertion that succeeds}{semantics-sasertok}{\semanticstests/SemanticsRule.SAssertOk.asl}

\ExampleDef{Evaluation of Assertions: Failure}
In \listingref{semantics-sassertno},
evaluating \texttt{assert (42 == 3);} results in an \DynamicAssertionFailure{} error.
\ASLListing{Evaluating an assertion that fails}{semantics-sassertno}{\semanticstests/SemanticsRule.SAssertNo.asl}


\RenderProseAndFormally{eval_stmt_SAssert}
\CodeSubsection{\EvalSAssertBegin}{\EvalSAssertEnd}{../Interpreter.ml}


\section{While Statements\label{sec:WhileStatements}}
\hypertarget{def-whilestatementterm}{}

\ASLListing{A \texttt{while} statement}{semantics-swhile}{\semanticstests/SemanticsRule.SWhile.asl}

\ConventionDef{Loop Limits}
Conventionally, all loop kinds should specify a limit expression.
For example, the loops in \listingref{semantics-swhile} specifies a limit via
the expression \verb|limit_loop()|.

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Twhile \parsesep \Nexpr \parsesep \Nlooplimit \parsesep \Tdo \parsesep \Nstmtlist \parsesep \Tend \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_while}


\ASTRuleDef{SWhile}
\begin{mathpar}
\inferrule{
  \buildexpr(\vlimitexpr) \astarrow \astversion{\vlimitexpr}\\
  \buildlooplimit(\voptlimit) \astarrow \astversion{\voptlimit}
}{
  {
    \begin{array}{r}
  \buildstmt\left(\overname{\Nstmt\left(
    \begin{array}{l}
    \Twhile, \econd: \Nexpr, \\
    \wrappedline\ \voptlimit : \Nlooplimit, \Tdo, \\
    \wrappedline\ \punnode{\Nstmtlist}, \Tend, \Tsemicolon
    \end{array}
    \right)}{\vparsednode}\right)
  \astarrow\\
  \overname{\SWhile(\astof{\vexpr}, \astversion{\voptlimit}, \astof{\vstmtlist})}{\vastnode}
\end{array}
}
}
\end{mathpar}

\ASTRuleDef{LoopLimit}
\NotImportedToASLSpecYet{
\hypertarget{build-looplimit}{}
The function
\[
\buildlooplimit(\overname{\parsenode{\Nlooplimit}}{\vparsednode}) \aslto \overname{\Option{\expr}}{\vastnode}
\]
transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule[limit]{}{
  \buildlooplimit\left(\overname{\Nlooplimit(\Tlooplimit, \punnode{\Nexpr})}{\vparsednode}\right)
  \astarrow
  \overname{\some{\astof{\vexpr}}}{\vastnode}
}
\end{mathpar}

\begin{mathpar}
\inferrule[no\_limit]{}{
  \buildlooplimit\left(\overname{\Nlooplimit(\emptysentence)}{\vparsednode}\right)
  \astarrow
  \overname{\none}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SWhile}
\ExampleDef{Typing While Loops}
The specification in \listingref{typing-swhile} is well-typed
and shows two \whilestatementterm{} --- the one in \verb|scan| contains a loop limit
and the one in \verb|main| does not contain a loop limit.
\ASLListing{Typing while statements}{typing-swhile}{\typingtests/TypingRule.SWhile.asl}

The specification in \listingref{typing-swhile-bad-limit}
is ill-typed, since the loop limit is not a \constrainedintegerterm.
\ASLListing{An ill-typed loop limit}{typing-swhile-bad-limit}{\typingtests/TypingRule.SWhile.bad_limit.asl}


\RenderProseAndFormally{annotate_stmt_SWhile}
\CodeSubsection{\SWhileBegin}{\SWhileEnd}{../Typing.ml}


\TypingRuleDef{AnnotateLimitExpr}
\RenderRelation{annotate_limit_expr}

\ExampleDef{Annotating Limit Expressions}
The specification in \listingref{typing-swhile} has two loops.
The loop in \verb|scan| is limited by the constrained integer
expression \verb|N|, while the loop in \verb|main| does not
have a loop limit.

The loop in \listingref{typing-swhile-bad-limit} uses
the limit expression \verb|i_limit| whose type the
\unconstrainedintegertypeterm, which is illegal for
limit expressions.


\RenderProseAndFormally{annotate_limit_expr}
\CodeSubsection{\AnnotateLimitExprBegin}{\AnnotateLimitExprEnd}{../Typing.ml}

\subsection{Semantics}
\SemanticsRuleDef{SWhile}
\ExampleDef{Evaluation of While Statements}
The specification in \listingref{semantics-swhile} prints the
following to the console:
% CONSOLE_BEGIN aslref \semanticstests/SemanticsRule.SWhile.asl
\begin{Verbatim}[fontsize=\footnotesize, frame=single]
i = 0
i = 1
i = 2
i = 3
\end{Verbatim}
% CONSOLE_END

The specification in \listingref{swhile-limit-reached} yields a dynamic
error once the loop limit for the \whilestatementterm{} is reached.
\ASLListing{Reaching a while loop limit}{swhile-limit-reached}{\semanticstests/SemanticsRule.SWhile.limit_reached.asl}


\RenderProseAndFormally{eval_stmt_SWhile}
\CodeSubsection{\EvalSWhileBegin}{\EvalSWhileEnd}{../Interpreter.ml}

\SemanticsRuleDef{Loop}
\RenderRelation{eval_loop}

More specifically, $\evalloop(\env, \iswhile, \velimitopt, \econd, \vbody)$
evaluates\\ $\vbody$ in $\env$ as long as $\econd$ holds when $\iswhile$ is $\True$
or until $\econd$ holds when $\iswhile$ is $\False$.
If the number of iterations exceeds the optional value specified by $\vlimitopt$,
the result is a \dynamicerrorterm{}.
The result is either the continuing configuration \\ $\Continuing(\newg,\newenv)$,
an early return configuration, or an abnormal configuration.

\ExampleDef{Evaluation of Loops}
The specification in \listingref{semantics-loop} does not result in any Assertion Error
and the specification terminates with exit code $0$.
\ASLListing{Evaluating a loop}{semantics-loop}{\semanticstests/SemanticsRule.Loop.asl}

In the following definition,
the premise $\vb \neq \iswhile$ is $\True$ in the case of a \texttt{while} loop
and the loop condition $\ve$ not holding, which is exactly when we want the
loop to exit. The opposite holds for a \texttt{repeat} loop.
The negation of the condition is used to decide whether to continue the loop iteration.

\RenderProseAndFormally{eval_loop}
\CodeSubsection{\EvalLoopBegin}{\EvalLoopEnd}{../Interpreter.ml}

\SemanticsRuleDef{EvalLimit}
\RenderRelation{eval_limit}

The evaluation uses the function $\evalexprsef$ because limit expressions are
guaranteed \sideeffectfreeterm{} by the typechecker,
see \TypingRuleRef{AnnotateLimitExpr}.

See \ExampleRef{Evaluation of While Statements} to see how the
limit expression is evaluated just once for the entire evaluation
of the \whilestatementterm.


\RenderProseAndFormally{eval_limit}

\SemanticsRuleDef{TickLoopLimit}
\RenderRelation{tick_loop_limit}

\ExampleDef{Decrementing a Loop Limit Value}
In \listingref{semantics-swhile}, the loop limit value
starts at $\nvint(4)$ and decrements towards $\nvint(0)$,
stopping at $\nvint(1)$ on the last iteration of the loop.

\ExampleDef{Negative Loop Limit Values}
In \listingref{semantics-swhile-negative-limit}, the loop limit value starts at $\nvint(-1)$
so the loop limit is immediately reached, resulting in a \dynamicerrorterm{} without executing the loop body at all.
(The same would happen if the loop limit value started at $\nvint(0)$.)
\ASLListing{A \texttt{while} statement with a negative loop limit}{semantics-swhile-negative-limit}{\semanticstests/SemanticsRule.SWhile.negative_limit.asl}

\RenderProseAndFormally{tick_loop_limit}

\section{Repeat Statements\label{sec:RepeatStatements}}
\hypertarget{def-repeatstatementterm}{}

\ASLListing{A repeat statement}{semantics-srepeat}{\semanticstests/SemanticsRule.SRepeat.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Trepeat \parsesep \Nstmtlist \parsesep \Tuntil \parsesep \Nexpr \parsesep \Nlooplimit \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_repeat}

\ASTRuleDef{SRepeat}
\begin{mathpar}
\inferrule{
  \buildexpr(\vlimitexpr) \astarrow \astversion{\vlimitexpr}
}{
  {
    \begin{array}{r}
  \buildstmt\left(\overname{\Nstmt\left(
    \begin{array}{r}
    \Tlooplimit, \Tlpar, \namednode{\vlimitexpr}{\Nexpr}, \Trpar, \Trepeat, \\
    \wrappedline\ \Nstmtlist, \Tuntil, \punnode{\Nexpr}, \punnode{\Nlooplimit}, \Tsemicolon
    \end{array}
    \right)}{\vparsednode}\right)
  \astarrow\\
  \overname{\SRepeat(\astof{\vstmtlist}, \astof{\vexpr}, \astof{\vlooplimit})}{\vastnode}
    \end{array}
  }
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SRepeat}
\ExampleDef{Typing a Repeat Statement}
The \repeatstatementsterm{} in \listingref{semantics-srepeat} are well-typed.


\RenderProseAndFormally{annotate_stmt_SRepeat}
\CodeSubsection{\SRepeatBegin}{\SRepeatEnd}{../Typing.ml}


\subsection{Semantics}
\SemanticsRuleDef{SRepeat}
\ExampleDef{Evaluation of Repeat Statements}
The specification in \listingref{semantics-srepeat} produces the following output to the console.
% CONSOLE_BEGIN aslref  --type-check-no-warn \semanticstests/SemanticsRule.SRepeat.asl
\begin{Verbatim}[fontsize=\footnotesize, frame=single]
j = 0
j = 1
j = 2
j = 3
j = 4
#ones in x = 5
i = 0
i = 1
i = 2
i = 3
i = 4
#ones in x = 5
\end{Verbatim}
% CONSOLE_END


\RenderProseAndFormally{eval_stmt_SRepeat}
\CodeSubsection{\EvalSRepeatBegin}{\EvalSRepeatEnd}{../Interpreter.ml}

\section{For Statements\label{sec:ForStatements}}
\hypertarget{def-forstatementterm}{}

\ASLListing{\texttt{for} loops}{semantics-sfor}{\semanticstests/SemanticsRule.SFor.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tfor \parsesep \Tidentifier \parsesep \Teq \parsesep \Nexpr \parsesep \Ndirection \parsesep
                    \Nexpr \parsesep \Nlooplimit \parsesep \Tdo &\\
                        & \wrappedline\ \Nstmtlist \parsesep \Tend \parsesep \Tsemicolon &\\
\Ndirection \derives \ & \Tto \;|\; \Tdownto &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_for}


\ASTRuleDef{SFor}
\begin{mathpar}
\inferrule{
  \buildexpr(\vstarte) \astarrow \astversion{\vstarte}\\
  \buildexpr(\vende) \astarrow \astversion{\vende}\\
}{
  {
    \begin{array}{r}
      \buildstmt\left(\overname{\Nstmt\left(
        \begin{array}{l}
        \Tfor, \Tidentifier(\vindexname), \Teq, \namednode{\vstarte}{\Nexpr},  \\
        \wrappedline\ \Ndirection, \namednode{\vende}{\Nexpr}, \punnode{\Nlooplimit}, \Tdo, \\
        \wrappedline\ \punnode{\Nstmtlist}, \Tend, \Tsemicolon
        \end{array}
        \right)}{\vparsednode}\right)
      \astarrow \\
        \overname{
        \SFor\left(\left\{
          \begin{array}{rcl}
            \Forindexname &:& \vindexname\\
            \Forstarte &:& \astversion{\vstarte}\\
            \Fordir &:& \astof{\vdirection}\\
            \Forende &:& \astversion{\vende}\\
            \Forbody &:& \astof{\vstmtlist}\\
            \Forlimit &:& \astof{\vlooplimit}\\
          \end{array}
            \right\}\right)
    }{\vastnode}
    \end{array}
  }
}
\end{mathpar}

\ASTRuleDef{Direction}
\NotImportedToASLSpecYet{
\hypertarget{build-direction}{}
The function
\[
\builddirection(\overname{\parsenode{\Ndirection}}{\vparsednode}) \;\aslto\; \overname{\fordirection}{\vastnode}
\]
transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule[to]{}{
  \builddirection(\overname{\Ndirection(\Tto)}{\vparsednode}) \astarrow \overname{\UP}{\vastnode}
}
\end{mathpar}

\begin{mathpar}
\inferrule[downto]{}{
  \builddirection(\overname{\Ndirection(\Tdownto)}{\vparsednode}) \astarrow \overname{\DOWN}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SFor}
The \texttt{for} loops in \listingref{semantics-sfor} are well-typed.

\ExampleDef{Ill-typed for loop}
\listingref{typing-forloop-bad1},
\listingref{typing-forloop-bad2},
\listingref{typing-forloop-bad3}, and
\listingref{typing-forloop-bad4}
show examples of ill-typed \texttt{for} loops.

\ASLListing{Ill-typed for loop 1}{typing-forloop-bad1}{\typingtests/TypingRule.SFor.bad1.asl}
\ASLListing{Ill-typed for loop 2}{typing-forloop-bad2}{\typingtests/TypingRule.SFor.bad2.asl}
\ASLListing{Ill-typed for loop 3}{typing-forloop-bad3}{\typingtests/TypingRule.SFor.bad3.asl}
\ASLListing{Ill-typed for loop 4}{typing-forloop-bad4}{\typingtests/TypingRule.SFor.bad4.asl}


\RenderProseAndFormally{annotate_stmt_SFor}
\CodeSubsection{\SForBegin}{\SForEnd}{../Typing.ml}


\TypingRuleDef{SForConstraints}
\RenderRelation{get_for_constraints}

\ExampleDef{Inferring the Constraints of a for Loop Index}
In \listingref{semantics-sfor} the constraints for the loop index variable
\verb|j| in \verb|scan| are \verb|0..N-1|,
and the constraints for the loop index variable \verb|i| in \verb|main| are \verb|0..4|.


\RenderProseAndFormally{get_for_constraints}

\subsection{Semantics}
\SemanticsRuleDef{SFor}
Evaluating a \texttt{for} statement involves introducing an index variable to the
environment. The type system ensures, via \TypingRuleRef{SFor}, that the index variable
is not already declared in the scope of the subprogram containing the \texttt{for}
statement.

\pagebreak % To avoid cutting the example output.
\ExampleDef{Evaluation of For Statements}
The specification in \listingref{semantics-sfor} is followed by its output to the console.
% CONSOLE_BEGIN aslref \semanticstests/SemanticsRule.SFor.asl
\begin{Verbatim}[fontsize=\footnotesize, frame=single]
j = 0
j = 1
j = 2
j = 3
j = 4
#ones in x = 5
i = 4
i = 3
i = 2
i = 1
i = 0
#ones in x = 5
\end{Verbatim}
% CONSOLE_END

The specification in \listingref{SFor-nop} shows a \forstatementterm{}
whose body does not evaluate since its lower bound is greater than its upper bound.
\ASLListing{A for loop with no iterations}{SFor-nop}{\semanticstests/SemanticsRule.SFor.nop.asl}

Recall that the expressions for the \texttt{for} loop range are
\sideeffectfreeterm{}, as guaranteed by \TypingRuleRef{SFor}, which is why
they are evaluated via $\evalexprsef$.

\RenderProseAndFormally{eval_stmt_SFor}
\CodeSubsection{\EvalSForBegin}{\EvalSForEnd}{../Interpreter.ml}

\SemanticsRuleDef{EvalFor}
\RenderRelation{eval_for}

\ExampleDef{Overall Evaluation of For Statements}
The specification in \listingref{semantics-sfor}
does not result in any assertion error, and terminates with exit-code $0$.

Evaluating $(\vindexname, \vstart, \dir, \vend, \vbody)$ in $\env$ yields either
a continuing configuration $\Continuing(\newg, \newenv)$, or a returning configuration
(in case the body of the loop results in an early return),
or an abnormal configuration.


\RenderProseAndFormally{eval_for}
\CodeSubsection{\EvalForBegin}{\EvalForEnd}{../Interpreter.ml}

\SemanticsRuleDef{EvalForLoop}
\RenderRelation{eval_for_loop}

See \ExampleRef{Overall Evaluation of For Statements}.


\RenderProseAndFormally{eval_for_loop}

\SemanticsRuleDef{EvalForStep}
\RenderRelation{eval_for_step}

See \ExampleRef{Overall Evaluation of For Statements}.

\RenderProseAndFormally{eval_for_step}

\hypertarget{def-throwstatementterm}{}
\section{Throw Statements\label{sec:ThrowStatements}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tthrow \parsesep \Nexpr \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_throw}


\ASTRuleDef{SThrow}
\begin{mathpar}
\inferrule{}{
  \buildstmt(\overname{\Nstmt(\Tthrow, \Nexpr, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SThrow(\astof{\vexpr})}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SThrow}
\listingref{semantics-sthrowsometyped}
shows examples of well-typed \throwstatementsterm.


\RenderProseAndFormally{annotate_stmt_SThrow}

\CodeSubsection{\SThrowBegin}{\SThrowEnd}{../Typing.ml}

\subsection{Semantics}
\SemanticsRuleDef{SThrow}
\ExampleDef{Throwing a Typed Exception}
The specification in \listingref{semantics-sthrowsometyped}
terminates successfully. That is, no \dynamicerrorterm{} occurs.
\ASLListing{Throwing an exception}{semantics-sthrowsometyped}{\semanticstests/SemanticsRule.SThrowSomeTyped.asl}


\RenderProseAndFormally{eval_stmt_SThrow}
\CodeSubsection{\EvalSThrowBegin}{\EvalSThrowEnd}{../Interpreter.ml}

\hypertarget{def-trystatementterm}{}
\section{Try Statements\label{sec:TryStatements}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Ttry \parsesep \Nstmtlist \parsesep \Tcatch \parsesep \ListOne{\Ncatcher} \parsesep \Notherwiseopt &\\
                  & \wrappedline\ \parsesep \Tend \parsesep \Tsemicolon &\\
\Notherwiseopt \derives\ & \Totherwise \parsesep \Tarrow \parsesep \Nstmtlist &\\
               |\ & \emptysentence &\\
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_try}


\ASTRuleDef{STry}
\begin{mathpar}
\inferrule{
  \buildlist[\Ncatcher] \astarrow \astversion{\vcatcherlist}
}{
  {
    \begin{array}{r}
  \buildstmt\left(\overname{\Nstmt\left(
    \begin{array}{r}
    \Ttry, \Nstmtlist, \Tcatch,  \\
    \wrappedline\ \namednode{\vcatcherlist}{\ListOne{\Ncatcher}}, \\
    \wrappedline\ \Notherwiseopt, \Tend, \Tsemicolon
    \end{array}
    \right)}{\vparsednode}\right)
  \astarrow \\
  \overname{\STry(\astof{\vstmtlist}, \astversion{\vcatcherlist}, \astof{\votherwiseopt})}{\vastnode}
\end{array}
}
}
\end{mathpar}

\ASTRuleDef{OtherwiseOpt}
\NotImportedToASLSpecYet{
\hypertarget{build-otherwiseopt}{}
The function
\[
   \buildotherwiseopt(\overname{\parsenode{\Notherwiseopt}}{\vparsednode}) \aslto
    \overname{\Option{\stmt}}{\vastnode}
\]
transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
} % END_OF_UNIMPORTED_RELATION


\begin{mathpar}
\inferrule[non\_empty]{
  \buildstmtlist(\vstmts) \astarrow \astversion{\vstmts}
}{
  {
  \begin{array}{r}
    \buildotherwiseopt(\overname{\Notherwiseopt(\Totherwise, \Tarrow, \namednode{\vstmts}{\Nstmtlist})}{\vparsednode}) \astarrow\\
    \astversion{\vstmts}
  \end{array}
  }
}
\end{mathpar}

\begin{mathpar}
\inferrule[empty]{}{
  \buildotherwiseopt(\overname{\Notherwiseopt(\emptysentence)}{\vparsednode}) \astarrow \none
}
\end{mathpar}

\subsection{Typing}

\TypingRuleDef{STry}
\ExampleDef{Typing Try Statements}
In
\listingref{semantics-catchnamed},
\listingref{semantics-catchotherwise},
\listingref{semantics-catchnone},
\listingref{semantics-nothrow}, and
\listingref{semantics-stry},
the \trystatementsterm{} are all well-typed.

\RenderProseAndFormally{annotate_stmt_STry}
\CodeSubsection{\STryBegin}{\STryEnd}{../Typing.ml}

\subsection{Semantics}
\SemanticsRuleDef{STry}
\ExampleDef{Evaluation of Try Statements}
Evaluating the specification in \listingref{semantics-stry}
does not result in any Assertion error, and the specification terminates with the exit code $0$.
\ASLListing{Evaluating a \texttt{try} statement}{semantics-stry}{\semanticstests/SemanticsRule.STry.asl}


\RenderProseAndFormally{eval_stmt_STry}
\CodeSubsection{\EvalSTryBegin}{\EvalSTryEnd}{../Interpreter.ml}

\hypertarget{def-returnstatementterm}{}
\section{Return Statements\label{sec:ReturnStatements}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Treturn \parsesep \option{\Nexpr} \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_return}

\ASTRuleDef{SReturn}
\begin{mathpar}
\inferrule{
  \buildoption[\Nexpr](\vexpr) \astarrow \astversion{\vexpr}
}{
  \buildstmt(\overname{\Nstmt(\Treturn, \namednode{\vexpr}{\option{\Nexpr}}, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SReturn(\astversion{\vexpr})}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SReturn}

\ExampleDef{Typing Return Statements}
The \returnstatementsterm{} in
\listingref{semantics-sreturn},
\listingref{semantic-ssreturnone}, and
\listingref{semantics-sreturntuple}
are all well-typed.

The return statement \verb|return 0;| in \listingref{typing-return-bad} is ill-typed,
since \verb|proc| is not a function but a procedure.
\ASLListing{An ill-typed return statement}{typing-return-bad}{\typingtests/TypingRule.SReturn.bad.asl}


\RenderProseAndFormally{annotate_stmt_SReturn}
\CodeSubsection{\SReturn}{\SReturnEnd}{../Typing.ml}


\subsection{Semantics}
\SemanticsRuleDef{SReturn}
\ExampleDef{No Return Value}
The specification in \listingref{semantics-sreturn} exits the procedure \texttt{println\_me}
by evaluating the\\ \texttt{return;} statement.
\ASLListing{Evaluating a \texttt{return} statement with no value}{semantics-sreturn}{\semanticstests/SemanticsRule.SReturnNone.asl}

\ExampleDef{Returning a Single Value}
In \listingref{semantic-ssreturnone},
\texttt{return 3;} exits the function \texttt{f} with value \texttt{3}.
\ASLListing{Evaluating a \texttt{return} statement with a single value}{semantic-ssreturnone}{\semanticstests/SemanticsRule.SReturnOne.asl}

\ExampleDef{Returning a Tuple of Values}
In \listingref{semantics-sreturntuple},
\texttt{return (3, 42);} exits the function \texttt{f} with the value \texttt{(3, 42)}.
\ASLListing{Evaluating a \texttt{return} statement with a tuple of values}{semantics-sreturntuple}{\semanticstests/SemanticsRule.SReturnSome.asl}


\RenderProseAndFormally{eval_stmt_SReturn}
\CodeSubsection{\SReturnBegin}{\EvalSReturnEnd}{../Interpreter.ml}

\SemanticsRuleDef{EExprListM}
\RenderRelation{eval_expr_list_m}

\ExampleDef{Seperately Evaluating a List of Expressions}
In \listingref{semantics-sreturntuple}, the expressions \verb|3| and \verb|42|
are evaluated in left-to-right order in the statement \verb|return (3 , 42);|.


\RenderProseAndFormally{eval_expr_list_m}

\SemanticsRuleDef{WriteFolder}
\RenderRelation{write_folder}

\ExampleDef{Folding a List of Pairs with Values and Execution Graphs}
In \listingref{semantics-sreturntuple}, the statement \verb|return (3 , 42);|
uses $\writefolder$ to generate \\
$([\nvint(3), \nvint(42)], \emptygraph)$.
The \executiongraphterm{} is empty, since literal expressions do not yield
\executiongraphsterm{} and composing empty \executiongraphsterm{} yields an
empty \executiongraphterm{}.


\RenderProseAndFormally{write_folder}

\hypertarget{def-printstatementterm}{}
\section{Print Statements\label{sec:PrintStatements}}
\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tprint \parsesep \ClistZero{\Nexpr} \parsesep \Tsemicolon & \\
\Nstmt \derives \ & \Tprintln \parsesep \ClistZero{\Nexpr} \parsesep \Tsemicolon & \\
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_print}


\ASTRuleDef{SPrint}
\begin{mathpar}
\inferrule{%
  \buildclist[\Nexpr](\vargs) \astarrow \astversion{\vargs} \\
  \vnewline \eqdef \False \\
}{%
  \buildstmt(\overname{\Nstmt(\Tprint, \namednode{\vargs}{\ClistZero{\Nexpr}}, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SPrint(\astversion{\vargs}, \vnewline)}{\vastnode}
}
\end{mathpar}

\begin{mathpar}
\inferrule{%
  \vparsednode = \Nstmt(\Tprintln, \namednode{\vargs}{\ClistZero{\Nexpr}}, \Tsemicolon)\\
  \buildclist[\Nexpr](\vargs) \astarrow \astversion{\vargs} \hva\\
  \vnewline \eqdef \True \\
  \vdebug \eqdef \False \\
}{%
  \buildstmt(\vparsednode) \astarrow
  \overname{\SPrint(\astversion{\vargs}, \vnewline)}{\vastnode}
}
\end{mathpar}

\subsection{Typing}
\TypingRuleDef{SPrint}
\listingref{literals1} shows literals and their corresponding types in comments.


\RenderProseAndFormally{annotate_stmt_SPrint}
\CodeSubsection{\SPrintBegin}{\SPrintEnd}{../Typing.ml}

\subsection{Semantics}
\SemanticsRuleDef{SPrint}

\ExampleDef{Printing Literals}
\listingref{semantics-literals} shows examples of printing various types of literals,
followed by the output to the console resulting from running the specification.
\ASLListing{Literals and how they are displayed}{semantics-literals}{\semanticstests/SemanticsRule.SPrint.asl}
% CONSOLE_BEGIN aslref \semanticstests/SemanticsRule.SPrint.asl
\begin{Verbatim}[fontsize=\footnotesize, frame=single]
string_number_1
0
1000000
53170898287292728730499578000
TRUE
FALSE
12345678900123456789/10000000000
0
hello\world
	 "here I am "
0xd
0x
LABEL_B
\end{Verbatim}
% CONSOLE_END

Notice that empty bitvectors are displayed as \verb|0x|.

We define the constant \RenderConstant{new_line}, which stands
for the newline character: $\vnewline \triangleq \ascii{10}$.

\RenderProseAndFormally{eval_stmt_SPrint}
\CodeSubsection{\EvalSPrintBegin}{\EvalSPrintEnd}{../Interpreter.ml}

Not all ASL runtimes support printing to a console (see \RequirementRef{Printing}).
%
Therefore, the semantics are parameterized by the following function.
\RenderRelation{output_to_console}

We now explain how printing is modelled when the runtime supports a console
(\SemanticsRuleRef{SupportedOutputToConsole})
and how it is modelled when the runtime does not support a console
(\SemanticsRuleRef{UnsupportedOutputToConsole}).

\SemanticsRuleDef{SupportedOutputToConsole}
To support a console, the definition of environments needs
to include an extra component to capture the string of characters sent to the console:
\[
\envs \triangleq \staticenvs \cartimes \dynamicenvs \cartimes \Strings \enspace.
\]
We omit this component in the rest of this document to avoid clutter, and include it
only here to explain the modeling of a console.

\ExampleRef{Printing Literals} shows the output to the console in a case it is supported.

\RenderRelation{literal_to_string}
The function is defined by \taref{literaltostringtable}.
%
Please note that surrounding quotations marks that appear in ASL text (for example, \verb|"hello"|)
are not included in string literals, and thus will not appear in the printed string.

\begin{table}
\caption{How literals should be represented as strings\label{ta:literaltostringtable}}
\begin{tabular}{rl}
\textbf{literal $\vl$} & \textbf{$\literaltostring(\vl)$} \\
\hline
$\LInt(n)$        & $n$ in decimal format, without any leading zeros, \\
                  & preceded by a ``\texttt{-}'' sign if $n$ is negative. \\
$\LBool(\True)$   & \texttt{TRUE} \\
$\LBool(\False)$  & \texttt{FALSE} \\
$\LReal(q)$       & $q$ as an irreducible fraction of positive integers, \\
                  & preceded by a ``\texttt{-}'' sign when $q$ is negative, \\
                  & with the denominator omitted if it is equal to 1. \\
$\LBitvector(b)$  & $b$ in hexadecimal, preceded by ``\texttt{0x}'', with enough leading \\
                  & zeros to make the number of hexadecimal digits printed \\
                  & equal to the width of $b$ divided by 4, and rounded up to \\
                  & the following integer.\\
$\LString(S)$     & $S$. \\
$\LLabel(s)$      & $s$. \\
\end{tabular}
\end{table}

\ProseParagraph
\AllApply
\begin{itemize}
  \item view $\env$ as the environment consisting of the \staticenvironmentterm{} $\tenv$,
        dynamic environment $\denv$, and console string $\vconsolestream$;
  \item view $\vv$ as a native literal for the literal $\vl$;
  \item \Proseeqdef{$\newenv$}{the environment consisting of the \staticenvironmentterm{} $\tenv$,
        dynamic environment $\denv$, and console string
        define as the concatenation of \\
        $\vconsolestream$ and $\literaltostring(\vl)$}.
\end{itemize}

\FormallyParagraph
\begin{mathpar}
\inferrule{
  \env \reverseeqdef (\tenv, \denv, \vconsolestream)\\
  \newenv \eqdef (\tenv, \denv, \vconsolestream \concat \literaltostring(\vl))
}{
  \outputtoconsole(\env, \NVLiteral(\vl)) \evalarrow (\newenv)
}
\end{mathpar}

\SemanticsRuleDef{UnsupportedOutputToConsole}
The function ignores the string value and returns the environment unchanged.

In a runtime without support for a console, the \printstatementsterm{}
in \listingref{semantics-literals} evaluate their list of expressions
with no other effect.

\ProseParagraph
\ProseEqdef{$\newenv$}{$\env$}.

\FormallyParagraph
\begin{mathpar}
\inferrule{}{
  \outputtoconsole(\env, \Ignore) \evalarrow \overname{\env}{\newenv}
}
\end{mathpar}

\section{The Unreachable Statement\label{sec:UnreachableStatement}}
\hypertarget{def-unreachablestatementterm}{}
\listingref{UnreachableStatement} shows an example of using an \unreachablestatementterm{}
to implement a custom form of assertion checking.
\ASLListing{An example use of an \texttt{unreachable} statement}{UnreachableStatement}{\definitiontests/UnreachableStatement.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tunreachable \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_unreachable}


\ASTRuleDef{SUnreachable}
\begin{mathpar}
\inferrule{}{
  \buildstmt(\overname{\Nstmt(\Tunreachable, \Tsemicolon)}{\vparsednode})
  \astarrow
  \overname{\SUnreachable}{\vastnode}
}
\end{mathpar}

\TypingRuleDef{SUnreachable}
\ExampleDef{Typing an Unreachable Statement}
The \unreachablestatementterm{} in \listingref{UnreachableStatement} is well-typed.

\RenderProseAndFormally{annotate_stmt_SUnreachable}

\SemanticsRuleDef{SUnreachable}
\ExampleDef{Evaluating an Unreachable Statement}
Evaluating the specification in \listingref{UnreachableStatement} results in a \dynamicerrorterm,
since the \unreachablestatementterm{} is evaluated.

\RenderProseAndFormally{eval_stmt_SUnreachable}

\section{Pragma Statements\label{sec:PragmaStatements}}
\hypertarget{def-pragmastatementterm}{}

\ASLListing{A pragma statement}{typing-spragma}{\typingtests/TypingRule.SPragma.asl}

\subsection{Syntax}
\begin{flalign*}
\Nstmt \derives \ & \Tpragma \parsesep \Tidentifier \parsesep \ClistZero{\Nexpr} \parsesep \Tsemicolon &
\end{flalign*}

\subsection{Abstract Syntax}
\RenderTypes[remove_hypertargets]{stmt_pragma}


\ASTRuleDef{SPragma}
\begin{mathpar}
\inferrule{
  \buildclist[\Nexpr](\vargs) \astarrow \astversion{\vargs}
}{
  {
  \begin{array}{r}
    \buildstmt(\overname{\Nstmt(\Tpragma, \Tidentifier(\id), \namednode{\vargs}{\ClistZero{\Nexpr}}, \Tsemicolon)}{\vparsednode})
  \astarrow \\
    \overname{\SPragma(\id, \astversion{\vargs})}{\vastnode}
  \end{array}
  }
}
\end{mathpar}

\TypingRuleDef{SPragma}
\ExampleDef{Typing a Pragma Statement}
The \pragmastatementterm{} in \listingref{typing-spragma} is well-typed.


\RenderProseAndFormally{annotate_stmt_SPragma}
\CodeSubsection{\SPragmaBegin}{\SPragmaEnd}{../Typing.ml}

\subsection{Semantics\label{sec:PragmaSemantics}}
Pragmas are structures present in the \untypedast{} that are designed to be used
by third-party tools.

To avoid conflicts between different ASL parsers, it is recommended that the pragma's identifier $\Tidentifier(\id)$ be prefixed by the name of the ASL tool that supports that pragma
(e.g. ARM for Arm's internal ASL tools). An ASL language processor that does not recognise a pragma directive should generate a warning for that pragma.

Pragmas are not associated with semantics and are discarded from the \typedast.