From 59be792c520599bca60d893db3bacff3bee88d4e Mon Sep 17 00:00:00 2001
From: Roman-Manevich <Roman.Manevich@arm.com>
Date: Sat, 23 Mar 2024 15:52:05 +0000
Subject: [PATCH] [asl][semantics] Addressing feedback.

---
 asllib/Interpreter.ml                         |   98 +-
 asllib/doc/ASLNotations.tex                   |   20 +-
 asllib/doc/ASLSemanticsReference.tex          | 2347 ++++++++++-------
 asllib/doc/ASLSyntaxReference.tex             |   21 +
 asllib/doc/ASLTypingReference.tex             |   27 +-
 asllib/doc/ASLmacros.tex                      |    7 +
 asllib/instrumentation.ml                     |    3 +
 .../SemanticsRule.EGetArrayTooSmall.asl       |    7 +-
 .../SemanticsRule.Lit.asl                     |    5 +-
 asllib/tests/ASLSemanticsReference.t/run.t    |    4 +-
 10 files changed, 1528 insertions(+), 1011 deletions(-)

diff --git a/asllib/Interpreter.ml b/asllib/Interpreter.ml
index 061c700a6d..ce89bf1a5f 100644
--- a/asllib/Interpreter.ml
+++ b/asllib/Interpreter.ml
@@ -392,17 +392,17 @@ module Make (B : Backend.S) (C : Config) = struct
     (* End *)
     (* Begin Binop *)
     | E_Binop (op, e1, e2) ->
-        let*^ m1, env' = eval_expr env e1 in
-        let*^ m2, new_env = eval_expr env' e2 in
+        let*^ m1, env1 = eval_expr env e1 in
+        let*^ m2, new_env = eval_expr env1 e2 in
         let* v1 = m1 and* v2 = m2 in
         let* v = B.binop op v1 v2 in
         return_normal (v, new_env) |: SemanticsRule.Binop
     (* End *)
     (* Begin Unop *)
-    | E_Unop (op, e') ->
-        let** v', env' = eval_expr env e' in
-        let* v = B.unop op v' in
-        return_normal (v, env') |: SemanticsRule.Unop
+    | E_Unop (op, e1) ->
+        let** v1, env1 = eval_expr env e1 in
+        let* v = B.unop op v1 in
+        return_normal (v, env1) |: SemanticsRule.Unop
     (* End *)
     (* Begin ECond *)
     | E_Cond (e_cond, e1, e2) ->
@@ -420,14 +420,14 @@ module Make (B : Backend.S) (C : Config) = struct
     (* Begin ESlice *)
     | E_Slice (e_bv, slices) ->
         let*^ m_bv, env1 = eval_expr env e_bv in
-        let*^ m_positions, env' = eval_slices env1 slices in
+        let*^ m_positions, new_env = eval_slices env1 slices in
         let* v_bv = m_bv and* positions = m_positions in
         let* v = B.read_from_bitvector positions v_bv in
-        return_normal (v, env') |: SemanticsRule.ESlice
+        return_normal (v, new_env) |: SemanticsRule.ESlice
     (* End *)
     (* Begin ECall *)
     | E_Call (name, actual_args, params) ->
-        let**| ms, env = eval_call (to_pos e) name env actual_args params in
+        let**| ms, new_env = eval_call (to_pos e) name env actual_args params in
         let* v =
           match ms with
           | [ m ] -> m
@@ -435,12 +435,12 @@ module Make (B : Backend.S) (C : Config) = struct
               let* vs = sync_list ms in
               B.create_vector vs
         in
-        return_normal (v, env) |: SemanticsRule.ECall
+        return_normal (v, new_env) |: SemanticsRule.ECall
     (* End *)
     (* Begin EGetArray *)
     | E_GetArray (e_array, e_index) -> (
         let*^ m_array, env1 = eval_expr env e_array in
-        let*^ m_index, env' = eval_expr env1 e_index in
+        let*^ m_index, new_env = eval_expr env1 e_index in
         let* v_array = m_array and* v_index = m_index in
         match B.v_to_int v_index with
         | None ->
@@ -449,20 +449,20 @@ module Make (B : Backend.S) (C : Config) = struct
             fatal_from e (Error.UnsupportedExpr e_index)
         | Some i ->
             let* v = B.get_index i v_array in
-            return_normal (v, env') |: SemanticsRule.EGetArray)
+            return_normal (v, new_env) |: SemanticsRule.EGetArray)
     (* End *)
     (* Begin ERecord *)
     | E_Record (_, e_fields) ->
         let names, fields = List.split e_fields in
-        let** v_fields, env' = eval_expr_list env fields in
+        let** v_fields, new_env = eval_expr_list env fields in
         let* v = B.create_record (List.combine names v_fields) in
-        return_normal (v, env') |: SemanticsRule.ERecord
+        return_normal (v, new_env) |: SemanticsRule.ERecord
     (* End *)
     (* Begin EGetField *)
     | E_GetField (e_record, field_name) ->
-        let** v_record, env' = eval_expr env e_record in
+        let** v_record, new_env = eval_expr env e_record in
         let* v = B.get_field field_name v_record in
-        return_normal (v, env') |: SemanticsRule.EGetBitField
+        return_normal (v, new_env) |: SemanticsRule.EGetBitField
     (* End *)
     (* Begin EGetFields *)
     | E_GetFields _ ->
@@ -470,15 +470,15 @@ module Make (B : Backend.S) (C : Config) = struct
     (* End *)
     (* Begin EConcat *)
     | E_Concat e_list ->
-        let** v_list, env' = eval_expr_list env e_list in
+        let** v_list, new_env = eval_expr_list env e_list in
         let* v = B.concat_bitvectors v_list in
-        return_normal (v, env') |: SemanticsRule.EConcat
+        return_normal (v, new_env) |: SemanticsRule.EConcat
     (* End *)
     (* Begin ETuple *)
     | E_Tuple e_list ->
-        let** v_list, env' = eval_expr_list env e_list in
+        let** v_list, new_env = eval_expr_list env e_list in
         let* v = B.create_vector v_list in
-        return_normal (v, env') |: SemanticsRule.ETuple
+        return_normal (v, new_env) |: SemanticsRule.ETuple
     (* End *)
     (* Begin EUnknown *)
     | E_Unknown t ->
@@ -487,9 +487,9 @@ module Make (B : Backend.S) (C : Config) = struct
     (* End *)
     (* Begin EPattern *)
     | E_Pattern (e, p) ->
-        let** v1, env' = eval_expr env e in
+        let** v1, new_env = eval_expr env e in
         let* v = eval_pattern env e v1 p in
-        return_normal (v, env') |: SemanticsRule.EPattern
+        return_normal (v, new_env) |: SemanticsRule.EPattern
   (* End *)
 
   (* Evaluation of Side-Effect-Free Expressions *)
@@ -646,22 +646,22 @@ module Make (B : Backend.S) (C : Config) = struct
     | LE_SetArray (re_array, e_index) ->
         let*^ rm_array, env1 = expr_of_lexpr re_array |> eval_expr env in
         let*^ m_index, env2 = eval_expr env1 e_index in
-        let m' =
+        let m1 =
           let* v = m and* v_index = m_index and* rv_array = rm_array in
           match B.v_to_int v_index with
           | None -> fatal_from le (Error.UnsupportedExpr e_index)
           | Some i -> B.set_index i v rv_array
         in
-        eval_lexpr ver re_array env2 m' |: SemanticsRule.LESetArray
+        eval_lexpr ver re_array env2 m1 |: SemanticsRule.LESetArray
     (* End *)
     (* Begin LESetField *)
     | LE_SetField (re_record, field_name) ->
         let*^ rm_record, env1 = expr_of_lexpr re_record |> eval_expr env in
-        let m' =
+        let m1 =
           let* v = m and* rv_record = rm_record in
           B.set_field field_name v rv_record
         in
-        eval_lexpr ver re_record env1 m' |: SemanticsRule.LESetField
+        eval_lexpr ver re_record env1 m1 |: SemanticsRule.LESetField
     (* End *)
     (* Begin LEDestructuring *)
     | LE_Destructuring le_list ->
@@ -712,8 +712,8 @@ module Make (B : Backend.S) (C : Config) = struct
     let eval_one env = function
       (* Begin SliceSingle *)
       | Slice_Single e ->
-          let** start, new_env = eval_expr env e in
-          return_normal ((start, one), new_env) |: SemanticsRule.SliceSingle
+          let** v_start, new_env = eval_expr env e in
+          return_normal ((v_start, one), new_env) |: SemanticsRule.SliceSingle
       (* End *)
       (* Begin SliceLength *)
       | Slice_Length (e_start, e_length) ->
@@ -727,19 +727,21 @@ module Make (B : Backend.S) (C : Config) = struct
           let*^ m_top, env1 = eval_expr env e_top in
           let*^ m_start, new_env = eval_expr env1 e_start in
           let* v_top = m_top and* v_start = m_start in
-          let* length = B.binop MINUS v_top v_start >>= B.binop PLUS one in
-          return_normal ((v_start, length), new_env) |: SemanticsRule.SliceRange
+          let* v_length = B.binop MINUS v_top v_start >>= B.binop PLUS one in
+          return_normal ((v_start, v_length), new_env) |: SemanticsRule.SliceRange
       (* End *)
       (* Begin SliceStar *)
       | Slice_Star (e_factor, e_length) ->
           let*^ m_factor, env1 = eval_expr env e_factor in
           let*^ m_length, new_env = eval_expr env1 e_length in
           let* v_factor = m_factor and* v_length = m_length in
-          let* start = B.binop MUL v_factor v_length in
-          return_normal ((start, v_length), new_env) |: SemanticsRule.SliceStar
+          let* v_start = B.binop MUL v_factor v_length in
+          return_normal ((v_start, v_length), new_env) |: SemanticsRule.SliceStar
       (* End *)
     in
-    fold_par_list eval_one env
+    (* Begin Slices *)
+    fold_par_list eval_one env |: SemanticsRule.Slices
+    (* End *)
 
   (* Evaluation of Patterns *)
   (* ---------------------- *)
@@ -761,18 +763,18 @@ module Make (B : Backend.S) (C : Config) = struct
     (* End *)
     (* Begin PGeq *)
     | Pattern_Geq e ->
-        let* v' = eval_expr_sef env e in
-        B.binop GEQ v v' |: SemanticsRule.PGeq
+        let* v1 = eval_expr_sef env e in
+        B.binop GEQ v v1 |: SemanticsRule.PGeq
     (* End *)
     (* Begin PLeq *)
     | Pattern_Leq e ->
-        let* v' = eval_expr_sef env e in
-        B.binop LEQ v v' |: SemanticsRule.PLeq
+        let* v1 = eval_expr_sef env e in
+        B.binop LEQ v v1 |: SemanticsRule.PLeq
     (* End *)
     (* Begin PNot *)
-    | Pattern_Not p' ->
-        let* b' = eval_pattern env pos v p' in
-        B.unop BNOT b' |: SemanticsRule.PNot
+    | Pattern_Not p1 ->
+        let* b1 = eval_pattern env pos v p1 in
+        B.unop BNOT b1 |: SemanticsRule.PNot
     (* End *)
     (* Begin PRange *)
     | Pattern_Range (e1, e2) ->
@@ -787,8 +789,8 @@ module Make (B : Backend.S) (C : Config) = struct
     (* End *)
     (* Begin PSingle *)
     | Pattern_Single e ->
-        let* v' = eval_expr_sef env e in
-        B.binop EQ_OP v v' |: SemanticsRule.PSingle
+        let* v1 = eval_expr_sef env e in
+        B.binop EQ_OP v v1 |: SemanticsRule.PSingle
     (* End *)
     (* Begin PMask *)
     | Pattern_Mask m ->
@@ -826,22 +828,22 @@ module Make (B : Backend.S) (C : Config) = struct
         >>= return_normal |: SemanticsRule.LDVar
     (* End *)
     (* Begin LDTyped *)
-    | LDI_Typed (ldi', _t), Some m ->
-        eval_local_decl s ldi' env (Some m) |: SemanticsRule.LDTyped
+    | LDI_Typed (ldi1, _t), Some m ->
+        eval_local_decl s ldi1 env (Some m) |: SemanticsRule.LDTyped
     (* End *)
     (* Begin LDUninitialisedTyped *)
-    | LDI_Typed (ldi', t), None ->
+    | LDI_Typed (ldi1, t), None ->
         let m = base_value env t in
-        eval_local_decl s ldi' env (Some m)
+        eval_local_decl s ldi1 env (Some m)
         |: SemanticsRule.LDUninitialisedTyped
     (* End *)
     (* Begin LDTuple *)
     | LDI_Tuple ldis, Some m ->
         let n = List.length ldis in
         let liv = List.init n (fun i -> m >>= B.get_index i) in
-        let folder envm ldi' vm =
+        let folder envm ldi1 vm =
           let**| env = envm in
-          eval_local_decl s ldi' env (Some vm)
+          eval_local_decl s ldi1 env (Some vm)
         in
         List.fold_left2 folder (return_normal env) ldis liv
         |: SemanticsRule.LDTuple
diff --git a/asllib/doc/ASLNotations.tex b/asllib/doc/ASLNotations.tex
index d87e6257ac..2a11163bb2 100644
--- a/asllib/doc/ASLNotations.tex
+++ b/asllib/doc/ASLNotations.tex
@@ -10,11 +10,15 @@
 The notation $\rightarrowfin$ stands for a function whose domain is finite.
 
 \begin{definition}[Function Update\label{def:FunctionUpdate}]
-  The notation $f[x \mapsto v]$ is the function $f$ modified so that $x$ is bound
-  to $v$: $f[x \mapsto v] \triangleq \lambda\ z.\ \begin{cases}
+  The notation $f[x \mapsto v]$ is a function identical to $f$, except that $x$ is bound
+  to $v$. That is, if  $g = f[x \mapsto v]$ then
+  \[
+    g(z) =
+  \begin{cases}
     f(z) & \text{if } z \neq x\\
     v & \text{if } z = x \enspace .
-  \end{cases}$
+  \end{cases}
+  \]
 
   The notation $\{i=1..k: a_i\mapsto b_i\}$ stands for the function formed from the corresponding input-output pairs:
   $\emptyfunc[a_1\mapsto b_1]\ldots[a_k\mapsto b_k]$.
@@ -42,9 +46,12 @@
 \paragraph{Rules}
 The following notation states that when the \emph{premises} $P_{1..k}$ hold then the \emph{verdict} $V$ holds as well:
 \begin{mathpar}
-  \inferrule{P_1 \and \ldots \and P_k}{V}
+  \inferrule[Name]{P_1 \and \ldots \and P_k}{V}
 \end{mathpar}
 That is, the premises of a rule are interpreted as a conjunction.
+%
+Optionally, the name of the rule, which is useful for referencing it, appears above and to the left of it.
+%
 The variables appearing in the premises and verdict are interpreted universally.
 %
 A set of rules is interpreted disjunctively. That is, each rule is used to determine whether its verdict
@@ -65,8 +72,9 @@
 
 \paragraph{Value Deconstruction}
 We will often want to deconstruct compound values to refer to their internal values.
-To achieve that, we will write $v \eqname \textit{deconstructed}(v)$ where the expression on the right
-exposes the internal structure of $v$, allowing us to alias its internal components.
+To achieve that, we will write $v \eqname \textit{f}(u_{1..k})$ where the expression on the right
+hand side exposes the internal structure of $v$, allowing us to alias its internal components
+via the new variables $u_{1..k}$.
 For example, suppose we know that $v$ is a pair of values.
 Then, $v \eqname (a, b)$ allows us to alias $a$ and $b$.
 Similarly, if $v$ is a non-empty list, then $v \eqname [h] + t$ deconstructs the list into the
diff --git a/asllib/doc/ASLSemanticsReference.tex b/asllib/doc/ASLSemanticsReference.tex
index 4997bf1865..d14cd4d6e2 100644
--- a/asllib/doc/ASLSemanticsReference.tex
+++ b/asllib/doc/ASLSemanticsReference.tex
@@ -5,14 +5,10 @@
 \newcommand\defref[1]{Def.~\ref{def:#1}}
 \newcommand\secref[1]{Section~\ref{sec:#1}}
 
-\newcommand\torexpr[0]{\textsf{rexpr}}
-\newcommand\semantic[1]{\llbracket #1 \rrbracket}
 \newcommand\tododefine[1]{\texttt{#1}}
 
 \usepackage{relsize}
-%\newcommand\eqname[0]{=}
 \newcommand\eqname[0]{\stackrel{\mathsmaller{\mathsf{name}}}{=}}
-%\newcommand\overname[2]{#1}
 \newcommand\overname[2]{\overbracket{#1}^{#2}}
 
 \newcommand\eq[0]{\textsf{eq}}
@@ -26,7 +22,7 @@
 \newcommand\WriteEffect[0]{\textsf{WriteEffect}}
 \newcommand\ReadEffect[0]{\textsf{ReadEffect}}
 
-\newcommand\emptyenv[0]{\underline{e}}
+\newcommand\emptyenv[0]{\env_{\emptyset}}
 \newcommand\tenv[0]{\textsf{tenv}}
 \newcommand\denv[0]{\textsf{denv}}
 \newcommand\denvtwo[0]{\textsf{denv2}}
@@ -64,6 +60,8 @@
 \newcommand\ThrowingConfig[0]{\texttt{\#T}}
 \newcommand\ErrorConfig[0]{\texttt{\#E}}
 \newcommand\OrAbnormal[0]{\terminateas \ThrowingConfig, \ErrorConfig}
+\newcommand\ProseOrAbnormal[0]{or an abnormal configuration, which short-circuits the entire evaluation}
+\newcommand\ProseOrError[0]{or an error configuration, which short-circuits the entire evaluation}
 \newcommand\TError[0]{\textsf{TError}}
 \newcommand\TThrowing[0]{\textsf{TThrowing}}
 \newcommand\TContinuing[0]{\textsf{TContinuing}}
@@ -109,12 +107,15 @@
 \newcommand\constantsvalues[1]{\text{constants\_values}}
 
 \newcommand\exprvals[0]{\textsf{ExprVals}}
+\newcommand\valuereadfrom[0]{\textsf{value\_read\_from}}
 \newcommand\Normal[0]{\textsf{Normal}}
 \newcommand\Throwing[0]{\textsf{Throwing}}
 \newcommand\Continuing[0]{\textsf{Continuing}}
 \newcommand\Returning[0]{\textsf{Returning}}
 \newcommand\Error[0]{\textsf{Error}}
 
+\newcommand\ErrorVal[1]{\Error(\texttt{"ERROR[#1]"})}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %% Names for variables appearing in rules
 
@@ -126,9 +127,9 @@
 \newcommand\envfour[0]{\texttt{env4}}
 \newcommand\envp[0]{\texttt{env'}}
 \newcommand\vc[0]{\texttt{c}}
-\newcommand\ve[0]{\texttt{e}}
 \newcommand\vi[0]{\texttt{i}}
 \newcommand\vg[0]{\texttt{g}}
+\newcommand\newg[0]{\texttt{new\_g}}
 \newcommand\vgp[0]{\texttt{g'}}
 \newcommand\vvp[0]{\texttt{v'}}
 \newcommand\vep[0]{\texttt{e'}}
@@ -136,17 +137,19 @@
 \newcommand\vm[0]{\texttt{m}}
 \newcommand\vn[0]{\texttt{n}}
 \newcommand\vp[0]{\texttt{p}}
+\newcommand\vpone[0]{\texttt{p1}}
 \newcommand\vv[0]{\texttt{v}}
-\newcommand\vx[0]{\texttt{x}}
+\newcommand\vy[0]{\texttt{y}}
 \newcommand\vs[0]{\texttt{s}}
 \newcommand\vt[0]{\texttt{t}}
+\newcommand\vtone[0]{\texttt{t1}}
 \newcommand\vu[0]{\texttt{u}}
 \newcommand\vw[0]{\texttt{w}}
 \newcommand\vvsg[0]{\texttt{vsg}}
 \newcommand\vvs[0]{\texttt{vs}}
 \newcommand\vms[0]{\texttt{ms}}
+\newcommand\vmsone[0]{\texttt{ms1}}
 \newcommand\vmstwo[0]{\texttt{ms2}}
-\newcommand\vle[0]{\texttt{le}}
 \newcommand\vles[0]{\texttt{les}}
 \newcommand\vre[0]{\texttt{re}}
 \newcommand\vres[0]{\texttt{res}}
@@ -167,7 +170,10 @@
 \newcommand\mcond[0]{\texttt{m\_cond}}
 \newcommand\vbv[0]{\texttt{v\_bv}}
 \newcommand\mpositions[0]{\texttt{m\_positions}}
+\newcommand\vslice[0]{\texttt{slice}}
+\newcommand\vsliceone[0]{\texttt{slice1}}
 \newcommand\slices[0]{\texttt{slices}}
+\newcommand\slicesone[0]{\texttt{slices1}}
 \newcommand\indices[0]{\texttt{indices}}
 \newcommand\positions[0]{\texttt{positions}}
 \newcommand\name[0]{\texttt{name}}
@@ -180,7 +186,6 @@
 \newcommand\nargsone[0]{\texttt{nargs1}}
 \newcommand\nargstwo[0]{\texttt{nargs2}}
 \newcommand\nargsthree[0]{\texttt{nargs3}}
-\newcommand\vargs[0]{\texttt{vargs}}
 \newcommand\vargsm[0]{\texttt{vargs\_m}}
 \newcommand\params[0]{\texttt{params}}
 \newcommand\earray[0]{\texttt{e\_array}}
@@ -209,6 +214,8 @@
 \newcommand\rvrecord[0]{\texttt{rv\_record}}
 \newcommand\vlelist[0]{\texttt{le\_list}}
 \newcommand\vmlist[0]{\texttt{vm\_list}}
+\newcommand\vlelistone[0]{\texttt{le\_list1}}
+\newcommand\vmlistone[0]{\texttt{vm\_list1}}
 \newcommand\nmonads[0]{\texttt{nmonads}}
 \newcommand\start[0]{\texttt{start}}
 \newcommand\mstart[0]{\texttt{m\_start}}
@@ -219,6 +226,7 @@
 \newcommand\length[0]{\texttt{length}}
 \newcommand\mlength[0]{\texttt{m\_length}}
 \newcommand\vlength[0]{\texttt{v\_length}}
+\newcommand\vdiff[0]{\texttt{v\_diff}}
 \newcommand\etop[0]{\texttt{e\_top}}
 \newcommand\vvtop[0]{\texttt{v\_top}}
 \newcommand\mtop[0]{\texttt{m\_top}}
@@ -227,7 +235,9 @@
 \newcommand\vfactor[0]{\texttt{v\_factor}}
 \newcommand\range[0]{\texttt{range}}
 \newcommand\ranges[0]{\texttt{ranges}}
+\newcommand\rangesone[0]{\texttt{ranges1}}
 \newcommand\ldi[0]{\texttt{ldi}}
+\newcommand\ldione[0]{\texttt{ldi1}}
 \newcommand\ldis[0]{\texttt{ldis}}
 \newcommand\liv[0]{\texttt{liv}}
 \newcommand\minitopt[0]{\texttt{m\_init\_opt}}
@@ -278,6 +288,8 @@
 \newcommand\velem[0]{\texttt{v\_elem}}
 \newcommand\vcs[0]{\texttt{cs}}
 \newcommand\bits[0]{\texttt{bits}}
+\newcommand\eid[0]{\texttt{e\_id}}
+\newcommand\newmbv[0]{\texttt{new\_m\_bv}}
 
 \input{ASLSemanticsLines}
 
@@ -386,7 +398,7 @@ \section{Mathematical Definitions and Notations}
 where $\None\triangleq\langle\rangle$ denotes an empty set
 and $\langle v \rangle$ denotes a set containing the single element $v$.
 %
-The notation $\langle T \rangle$, where $T$ denotes a mathematical types of values, stands for
+The notation $\langle T \rangle$, where $T$ denotes a mathematical type, stands for
 $\{ \langle\rangle \} \cup \{\langle v \rangle \;|\; v \in T\}$.
 
 \paragraph{Miscellaneous}
@@ -511,9 +523,11 @@ \subsection{Concurrent Execution Graphs \label{sec:concurrentexecutiongraphs}}
 
 The concurrent semantics of an ASL specification utilizes \emph{concurrent execution graphs}
 (\emph{execution graphs}, for short),
-which track the Read and Write Effects over variables, yielded by the sequential semantics, and the \emph{ordering constraints}
-between those effects.
-Concurrent execution graphs are introduced, defined, and used in~\cite{AlglaveMT14,alglave2016syntax,AlglaveDGHM21},
+which track the Read and Write Effects over variables, yielded by the sequential semantics,
+and the \emph{ordering constraints} between those effects.
+The graphs resulting from executing an ASL specification are converted into
+\emph{candidate execution graphs}, which are introduced, defined,
+and used in~\cite{AlglaveMT14,alglave2016syntax,AlglaveDGHM21}.
 
 Formally, an execution graph $\xgraph = (N^\xgraph, E^\xgraph, O^\xgraph) \in \XGraphs$
 is defined via a set of \emph{nodes} ($N^\xgraph$), \emph{edges} ($E^\xgraph$), and \emph{output nodes} ($O^\xgraph$):
@@ -528,7 +542,7 @@ \subsection{Concurrent Execution Graphs \label{sec:concurrentexecutiongraphs}}
 Nodes represent unique Read and Write Effects. Formally, a node $(u,l,\id)$ associates a unique instance counter $u$
 to an \emph{ordering label} $l$, which specifies whether it represents a Read Effect of a Write Effect to a variable named $\id$.
 %
-We say that en Effect $E_1$ is \emph{$l$-before} another Effect $E_2$, for $l\in \Labels$ and a given execution graph
+We say that en Effect \texttt{E1} is \emph{$l$-before} another Effect \texttt{E2}, for $l\in \Labels$ and a given execution graph
 $g$, when $(\texttt{E1}, l, \texttt{E2}) \in E^g$.
 
 An edge represents an ordering constraint between two effects, which can be one of the following:
@@ -607,9 +621,15 @@ \subsection{Input Configurations and Output Configurations}
   \item $\Normal((\vals\times\XGraphs)^*, \envs)$.
   \end{itemize}
 
-  \item[Exceptions.] Configurations in $\Throwing((\langle\vals \times \ty\rangle \times \XGraphs, \envs)$
-  represent thrown exceptions,
-  either without an exception value (as in \texttt{throw;}) or ones with an exception value and an associated type.
+  \item[Exceptions.] Configurations in
+  \[
+    \Throwing((\langle \valuereadfrom(\vals,\identifier) \times \ty\rangle \times \XGraphs, \envs)
+  \]
+  represent thrown exceptions.
+  There are two flavors of exceptions:
+  exceptions without an exception value (as in \texttt{throw;}), and ones with an exception value,
+  an identifier to which the read effect is attributed, and an associated type.
+  The type $\valuereadfrom(\vals,\identifier)$ is a configuration nested inside
   The ASL semantics propagates these \emph{exceptional configurations} to the nearest catch clause that matches
   them, and otherwise they are ``caught'' at the top-level and reported as errors (see dynamic errors below).
 
@@ -626,8 +646,8 @@ \subsection{Input Configurations and Output Configurations}
   represent runtime errors (for example, division by zero).
   The ASL semantics is set up such that when these \emph{error configurations} appear,
   the evaluation of the entire specification terminates by outputting them.
-  The actual strings in an error configuration are not considered part of the specification.
-  That is, an implementation of the semantics may use other strings.
+  Every implementation of this semantics must start with the strings appearing in this
+  semantics and optionally end with a longer description of the error.
 \end{description}
 Helper relations often have output configurations that are just tuples, without an associated domain.
 
@@ -653,7 +673,7 @@ \subsection{Input Configurations and Output Configurations}
 
 \subsection{Extracting and Substituting Elements of Configurations}
 
-We define the \emph{domain} of a configuration $C=M(\ldots)$, denoted $\configdomain{C}$, to be $M$.
+We define the \emph{domain} of a configuration $C=D(\ldots)$, denoted $\configdomain{C}$, to be $D$.
 
 Given a configuration $C$, we define the graph component of the configuration, $\graphof{C}$,
 and the environment of the configuration, $\environof{C}$, as follows:
@@ -667,7 +687,7 @@ \subsection{Extracting and Substituting Elements of Configurations}
   \Normal(\vg, \env) & \vg & \env\\
   \Normal([\vv_{1..k}], \vg) & \vg & \env\\
   \Normal([i=1..k: (\vv_i,\vg_i)], \env) & \text{undefined} & \env\\
-  \Throwing((\vx,\vg), \env) & \vg & \env\\
+  \Throwing((\valuereadfrom(\vx,\vv),\vg), \env) & \vg & \env\\
   \Returning(([\vv_{1..k}],\vg), \env) & \vg & \env\\
   \Continuing(\vg, \env) & \vg & \env\\
 \end{array}
@@ -685,7 +705,7 @@ \subsection{Extracting and Substituting Elements of Configurations}
   \Normal(\vg, \env) & \Normal(\vgp, \env)\\
   \Normal(i=1..k: \vv_i, \vg) & \Normal(i=1..k: \vv_i, \vgp)\\
   \Normal([i=1..k: (\vv_i,\vg_i)], \env) & \text{undefined}\\
-  \Throwing((\vx,\vg), \env) & \Throwing((\vx,\vgp), \env)\\
+  \Throwing((\valuereadfrom(\vx,\vv),\vg), \env) & \Throwing((\valuereadfrom(\vx,\vv),\vgp), \env)\\
   \Returning((i=1..k: \vv_i,\vg), \env) & \Returning((i=1..k: \vv_i,\vgp), \env)\\
   \Continuing(\vg, \env) & \Continuing(\vgp, \env)\\
 \end{array}
@@ -702,7 +722,7 @@ \subsection{Extracting and Substituting Elements of Configurations}
   \Normal(\vg, \env) & \Normal(\vg, \envp)\\
   \Normal(i=1..k: \vv_i, \vg) & \Normal(i=1..k: \vv_i, \vg)\\
   \Normal([i=1..k: (\vv_i,\vg_i)], \env) & \Normal([i=1..k: (\vv_i,\vg_i)], \envp)\\
-  \Throwing((\vx,\vg), \env) & \Throwing((\vx,\vg), \envp)\\
+  \Throwing((\valuereadfrom(\vx,\vv),\vg), \env) & \Throwing((\valuereadfrom(\vx,\vv),\vg), \envp)\\
   \Returning((i=1..k: \vv_i,\vg), \env) & \Returning((i=1..k: \vv_i,\vg), \envp)\\
   \Continuing(\vg, \env) & \Continuing(\vg, \envp)\\
 \end{array}
@@ -711,23 +731,13 @@ \subsection{Extracting and Substituting Elements of Configurations}
 \section{Semantic Evaluation}
 
 The semantics of ASL is given by the relations\footnote{The reason that relations, rather than functions, are used is due to the
-potential non-determinism in the primitive subprograms,
-the choice of execution graph node identifiers,
+potential non-determinism in the primitive subprograms
 and the non-determinism inherent in the \texttt{UNKOWN} expression.}
 $\evalarrow$ and $\evalprimitivearrow$.
-The latter relation provides the semantics of primitive functions and is not otherwise defined
+The latter relation provides the semantics of primitive subprograms and is not otherwise defined
 constructively.
 The relation $\evalarrow$ is defined as the disjoint union of the relations defined in this document.
-% \[
-%   \begin{array}{rcl}
-%   \evalarrow &\triangleq& \textit{main\_asl\_relations} \cupdot \textit{secondary\_asl\_relations}\\
-%   \textit{main\_asl\_relations} &\triangleq& \texttt{eval\_expr} \cupdot \texttt{eval\_lexpr} \cupdot \texttt{eval\_slices}\\
-%    & & \texttt{eval\_pattern} \cupdot \texttt{eval\_local\_decl} \cupdot \texttt{eval\_stmt}\\
-%    & & \texttt{eval\_block} \cup \texttt{eval\_loop}\\
-%    & & \texttt{eval\_catchers} \cupdot \texttt{eval\_call} \cupdot \texttt{eval\_spec}\\
-%    \textit{secondary\_asl\_relations} &\triangleq& ...
-%   \end{array}
-% \]
+%
 The semantics of the various types of AST nodes is given by a set of \emph{semantic relations} between
 input configurations and output configurations.
 
@@ -779,13 +789,6 @@ \section{Semantic Evaluation}
 
   We use the notation $C \evalarrow C'$ to denote a transition between input and output configurations.
   That is, $(C, C') \in\ \evalarrow$.
-%  We denote elements of a semantic relation by $\texttt{eval\_<label>}(\env, n) \evalarrow L'(v'_{1..n})$.
-%We define the semantic relation $\semantic{\texttt{label}}$, for each label, as
-% the set of all its semantic transitions:
-% \[
-%   \semantic{\texttt{label}} \triangleq \{ \texttt{eval\_<label>}(\env, n) \evalarrow L'(v'_{1..n})  \;|\;
-% \env \in \envs,\; \texttt{label}(n) \} \enspace.
-% \]
 
   When introducing semantic relations, instead of using the mathematical notation
   \[
@@ -811,7 +814,8 @@ \section{Semantic Evaluation}
   the output value and the output execution graph, respectively.
 
 \subsection{Natural Operational Semantics}
-We define the ASL semantics in the style of \emph{natural operational semantics}~\cite{SemanticsWithApplicationsBook}.
+We define the ASL semantics in the style of \emph{natural operational semantics}~\cite{SemanticsWithApplicationsBook}
+(also known as \emph{big step semantics}).
 Natural operational semantics evaluates the AST inductively.
 That is, it concludes transitions for configurations starting from
 non-leaf AST nodes by concluding transitions from configurations starting from their children nodes.
@@ -822,15 +826,21 @@ \subsection{Natural Operational Semantics}
 with more premises and so on.)
 
 \subsubsection{Evaluation Example}
+\newcommand\elint[1]{\texttt{E\_Literal}(\lint(#1))}
 
 The example shows how the rules for expression literals and binary operator expressions can be combined
-to infer a transition from an input configuration with the expression for $(1+2)*(4+5)$ to an output configuration
-with the value resulting from the calculation of the expression.
+to conclude a transition from an input configuration with the expression $(1+2)*(4+5)$,
+given by the AST
+\[
+  \begin{array}{rl}
+  \texttt{E\_Binop}(\MUL, &\texttt{E\_Binop}(\PLUS, \elint{1}, \elint{2}), \\
+                          & \texttt{E\_Binop}(\PLUS, \elint{4}, \elint{5}))
+  \end{array}
+\]
+to an output configuration with the value resulting from the calculation of the expression.
 
 For succinctness, we write $E(\texttt{<expression>})$
 for the AST node parsed from an expression $\texttt{<expression>}$.
-% That is, for an integer $n$, $E(n) \triangleq\texttt{E\_Literal}(\lint(n))$
-% and
 %
 We write $\emptyenv$ to stand for a trivial environment (that is, one where all functions are empty).
 
@@ -845,13 +855,11 @@ \subsubsection{Evaluation Example}
 Finally, the the transitions for both of the sub-expressions are used as premises for the binary expression
 rule, along with the rule for binary operator (for multiplication), to evaluate the entire expression.
 
-\newcommand\elint[1]{\texttt{E\_Literal}(\lint(#1))}
-
 \begin{mathpar}
   \inferrule*[right=\ref{sec:SemanticsRule.Binop}]{
     \inferrule*[right=\ref{sec:SemanticsRule.Lit}]{}{ \evalexpr{\emptyenv, E(1)} \evalarrow \Normal(\nvint(1), \emptyenv) } \\\\
     \inferrule*[right=\ref{sec:SemanticsRule.Lit}]{}{ \evalexpr{\emptyenv, E(2)} \evalarrow \Normal(\nvint(2), \emptyenv) } \\\\
-    \inferrule*[right=\ref{sec:BinaryOperator}]{}{\binop(\PLUS, \nvint(1), \nvint(2)) \evalarrow \nvint(3)}
+    \inferrule*[right=\ref{sec:SemanticsRule.BinopOperator}]{}{\binop(\PLUS, \nvint(1), \nvint(2)) \evalarrow \nvint(3)}
   }
   {
     \evalexpr{ \emptyenv, E(1+2) } \evalarrow
@@ -863,7 +871,7 @@ \subsubsection{Evaluation Example}
   \inferrule*[right=\ref{sec:SemanticsRule.Binop}]{
     \inferrule*[right=\ref{sec:SemanticsRule.Lit}]{}{ \evalexpr{\emptyenv, E(4)} \evalarrow \Normal(\nvint(4), \emptyenv) } \\\\
     \inferrule*[right=\ref{sec:SemanticsRule.Lit}]{}{ \evalexpr{\emptyenv, E(5)} \evalarrow \Normal(\nvint(5), \emptyenv) } \\\\
-    \inferrule*[right=\ref{sec:BinaryOperator}]{}{\binop(\PLUS, \nvint(4), \nvint(5)) \evalarrow \nvint(9)}
+    \inferrule*[right=\ref{sec:SemanticsRule.BinopOperator}]{}{\binop(\PLUS, \nvint(4), \nvint(5)) \evalarrow \nvint(9)}
   }
   {
     \evalexpr{ \emptyenv, E(4+5) } \evalarrow
@@ -875,7 +883,7 @@ \subsubsection{Evaluation Example}
   \inferrule*[right=\ref{sec:SemanticsRule.Binop}]{
     \evalexpr{ \emptyenv, E(1+2) } \evalarrow \Normal(\nvint(3), \emptyenv)\\
     \evalexpr{ \emptyenv, E(4+5) } \evalarrow \Normal(\nvint(9), \emptyenv)\\
-    \inferrule*[right=\ref{sec:BinaryOperator}]{}{\binop(\MUL, \nvint(3), \nvint(9)) \evalarrow \nvint(27)}
+    \inferrule*[right=\ref{sec:SemanticsRule.BinopOperator}]{}{\binop(\MUL, \nvint(3), \nvint(9)) \evalarrow \nvint(27)}
   }
   {
     \evalexpr{ \emptyenv, E((1+2)*(4+5)) } \evalarrow
@@ -884,8 +892,8 @@ \subsubsection{Evaluation Example}
 \end{mathpar}
 
 \subsubsection{No Undefined Behaviors}
-This semantics is defined for well-typed ASL specifications.
-This semantics gets stuck only in cases of non-terminating executions
+The ASL semantics is defined for well-typed ASL specifications
+and gets stuck only in cases of non-terminating executions
 (for example, non-terminating loops, or infinite recursion).
 Otherwise, for every input configuration there is at least one rule that can be used to take a semantic transition.
 
@@ -893,81 +901,98 @@ \subsection{Short-Circuit Rule Templates}
 
 Short-circuit rule templates allow us to succinctly define sets of rules.
 Specifically, they allow us to capture situations where if a transition
-into an output configuration occurs in a premise then the rest of the rule
-can be ignored as the input configuration in the verdict also transitions
+into an output configuration occurs in a premise then the rest of the premises
+are ignored, as the input configuration in the verdict also transitions
 into that output configuration. These output configurations are usually
 due to raised exceptions or dynamic errors.
 
-A template rule:
+\newcommand\XP[0]{\mathit{XP}}
+\newcommand\XQ[0]{\mathit{XQ}}
+
+In the following, $\XP$ and $\XQ$ stands for, possibly empty, sequences of premises.
+%
+A template rule including the special premise $C \evalarrow C' \terminateas E$,
+which introduces alternative output configurations $C'$ and $E$:
 \begin{mathpar}
   \inferrule{
-    i=1..k: P_i\\\\
+    \XP\\\\
     C \evalarrow C' \terminateas E\\\\
-    j=1..n: Q_i\\
+    \XQ\\
   }
   {
-    D \evalarrow D'
+    V \evalarrow V'
   }
 \end{mathpar}
-
-Stands for the following pair of rules (the second of which is possibly a template rule itself):
+stands for the following pair of rules (the second of which is possibly a template rule itself):
 \begin{mathpar}
-  \inferrule[(Short-circuited)]{
-    i=1..k: P_i\\\\
-    C \evalarrow E
+  \inferrule[(Option 1)]{
+    \XP\\\\
+    C \evalarrow C' \\\\
+    \XQ\\
   }
   {
-    D \evalarrow E
+    V \evalarrow V'
   }
-\and
-  \inferrule{
-    i=1..k: P_i\\\\
-    C \evalarrow C' \\\\
-    j=1..n: Q_i\\
+  \and
+  \inferrule[(Option 2:Short-circuited)]{
+    \XP\\\\
+    C \evalarrow E
   }
   {
-    D \evalarrow D'
+    V \evalarrow E
   }
 \end{mathpar}
-
-We allow several short-cirtcuiting configurations in a template.
-Specifically, a template rule:
+That is, if $C$ transitions to $C'$ then `$\sslash E$' can be ignored
+and the rule is interpreted as usual (Option 1).
+However, if $C$ transitions into $E$ (Option 2) then the premises $\XQ$ are ignored,
+thereby ``short-circuiting'' the rule, and the input configuration
+in the verdict also transitions into $E$.
+
+We allow more than one premise to include short-circuiting alternatives and also
+a single premise to include several alternatives
+That is, a template rule:
 \begin{mathpar}
   \inferrule{
-    i=1..k: P_i\\\\
+    \XP\\\\
     C \evalarrow C' \terminateas E_{1...m}\\\\
-    j=1..n: Q_i\\
+    \XQ\\
   }
   {
-    D \evalarrow D'
+    V \evalarrow V'
   }
 \end{mathpar}
 Stands for the set of template rules
 \begin{mathpar}
   \inferrule{
-    i=1..k: P_i\\\\
+    \XP\\\\
     C \evalarrow C' \terminateas E_1\\\\
-    j=1..n: Q_i\\
+    \XQ\\
   }
   {
-    D \evalarrow D'
+    V \evalarrow V'
   }
 \and
 \inferrule{\ldots}{}
 \and
 \inferrule{
-  i=1..k: P_i\\\\
+  \XP\\\\
   C \evalarrow C' \terminateas E_m\\\\
-  j=1..n: Q_i\\
+  \XQ\\
 }
 {
-  D \evalarrow D'
+  V \evalarrow V'
 }
 \end{mathpar}
 
+Notice that after all templates are expanded into normal rules,
+they behave like normal rules where the order of premises does
+not matter.
+
 We introduce the following shorthands for abnormal configurations:
 $\ThrowingConfig \triangleq \Throwing((\vv, \vg), \newenv)$
-and $\ErrorConfig \triangleq \Error(\vs)$.
+and $\ErrorConfig \triangleq \Error(\vs)$ where $\vv$, $\vg$, and $\vs$
+are fresh variables (that is, different from all other variables appearing
+in a rule).
 
 % \subsection{ASL Semantic Rules}
 
@@ -990,25 +1015,29 @@ \subsection{Short-Circuit Rule Templates}
 % Specifications & Chapter~\ref{chap:eval_spec}\\
 % \end{tabular}\\
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Reading guide}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 The set of rules for each label is further split according to the ``shape'' of the AST node.
 For example, expressions are split into literal expressions, binary operation expressions, etc.
 Each such subset of rules is named accordingly and appears in a section with the same name.
-For example, the rule for literal expressions is named SemanticsRule.Lit and defined in
-Section~\ref{sec:SemanticsRule.Lit}.
+For example, the rule for literal expressions is named SemanticsRule.Lit\footnote{Sometimes rules are split into cases.
+We then drop the SemanticsRule prefix from each case, for succinctness.
+The same convention applies to helper rules.} and defined in
+\secref{SemanticsRule.Lit}.
 
 Each rule is presented using the following template:
 \begin{itemize}
 \item a Prose paragraph gives the rule in English, and corresponds, as much as possible, to the code of the reference implementation ASLRef given at
  \href{https://github.com/herd/herdtools7//tree/master/asllib}{/herdtools7/asllib};
-\item one or several Example, which as much as possible are also given as regression tests in
+\item one or several Example, which, as much as possible, are also given as regression tests in
 \href{https://github.com/herd/herdtools7//tree/master/asllib/tests/ASLSemanticsReference.t}{/herdtools7/asllib/tests/ASLSemanticsReference.t};
 \item a Code paragraph which gives a verbatim of the corresponding implementation in the interpreter of ASLRef
 \href{https://github.com/herd/herdtools7//tree/master/asllib/Interpreter.ml}{/herdtools7/asllib/Interpreter.ml};
 \item a Formal paragraph, which provides semantic rules that essentially give the same information as the Prose paragraph, for both
 the sequential semantics and the concurrent semantics, in the form of concurrent execution graphs.
-The latter enables building, for each AArch64 instruction,
+The latter enables defining, for each AArch64 instruction,
 the Intrinsic dependencies used by the AArch64 memory model from the ASL code of the instruction~\cite[B2.3.2]{ArmARM}.
 \end{itemize}
 
@@ -1018,6 +1047,8 @@ \chapter{Basic Utility Relations \label{chap:utility}}
 
 In this chapter, we define helper relations for operating on native values,
 environments, and operations involving values and types.
+%
+In this chapter rules are presented without examples and the corresponding code.
 
 \newcommand\declarelocalidentifier[0]{\texttt{declare\_local\_identifier}}
 \newcommand\declarelocalidentifierm[0]{\texttt{declare\_local\_identifier\_m}}
@@ -1039,86 +1070,133 @@ \chapter{Basic Utility Relations \label{chap:utility}}
 \newcommand\basevalue[0]{\texttt{base\_value}}
 \newcommand\isvaloftype[0]{\texttt{is\_val\_of\_type}}
 
-\section{Dropping an Identifier from the Local Storage}
+We now define the following relations:
+\begin{itemize}
+  \item SemanticsRule.RemoveLocal \secref{SemanticsRule.RemoveLocal};
+  \item SemanticsRule.ReadIdentifier \secref{SemanticsRule.ReadIdentifier};
+  \item SemanticsRule.WriteIdentifier \secref{SemanticsRule.WriteIdentifier};
+  \item SemanticsRule.CreateBitvector \secref{SemanticsRule.CreateBitvector};
+  \item SemanticsRule.ConcatBitvectors \secref{SemanticsRule.ConcatBitvectors};
+  \item SemanticsRule.ReadFromBitvector \secref{SemanticsRule.ReadFromBitvector};
+  \item SemanticsRule.WriteToBitvector \secref{SemanticsRule.WriteToBitvector};
+  \item SemanticsRule.GetIndex \secref{SemanticsRule.GetIndex};
+  \item SemanticsRule.SetIndex \secref{SemanticsRule.SetIndex};
+  \item SemanticsRule.GetField \secref{SemanticsRule.GetField};
+  \item SemanticsRule.SetField \secref{SemanticsRule.SetField};
+  \item SemanticsRule.DeclareLocalIdentifier \secref{SemanticsRule.DeclareLocalIdentifier};
+  \item SemanticsRule.DeclareLocalIdentifierM\secref{SemanticsRule.DeclareLocalIdentifierM};
+  \item SemanticsRule.DeclareLocalIdentifierMM \secref{SemanticsRule.DeclareLocalIdentifierMM};
+  \item SemanticsRule.DeclareGlobal \secref{SemanticsRule.DeclareGlobal};
+  \item SemanticsRule.BaseValue \secref{SemanticsRule.BaseValue};
+\end{itemize}
+
+\section{SemanticsRule.RemoveLocal \label{sec:SemanticsRule.RemoveLocal}}
+\subsection{Prose}
 The relation
 \[
-  \removelocal(\overname{\envs}{\env} \aslsep \overname{\identifier}{\name}) \;\aslrel\; \overname{\envs}{\envp}
+  \removelocal(\overname{\envs}{\env} \aslsep \overname{\identifier}{\name}) \;\aslrel\; \overname{\envs}{\newenv}
 \]
-unmaps the identifier $\name$ from the local storage of the environment $\env$.
-We use the notation $[\name\mapsto\bot]$ to mean that $\name$ is no part of the domain of the resulting function.
+removes the binding of the identifier $\name$ from the local storage of the environment $\env$.
+
+Removal of the the identifier $\name$ from the local storage of the environment $\env$
+is the environment $\newenv$ and all of the following apply:
+\begin{itemize}
+  \item $\env$ consists of the static environment $\tenv$ and dynamic environment $\denv$;
+  \item $\newenv$ consists of the static environment $\tenv$ and the dynamic environment
+  with the same global component as $\denv$ --- $G^\denv$, and local compoenent $L^\denv$,
+  with the identifier $\name$ removed from its domain.
+\end{itemize}
+
+\begin{emptyformal}
+\subsection{Formally}
+  We use the notation $[\name\mapsto\bot]$ to mean that $\name$ is not in the domain of the resulting function.
 \begin{mathpar}
   \inferrule{
     \env \eqname (\tenv, (G^\denv, L^\denv))\\
-    \envp = (\tenv, (G^\denv, L^\denv[\name \mapsto \bot]))
+    \newenv = (\tenv, (G^\denv, L^\denv[\name \mapsto \bot]))
   }
   {
-    \removelocal(\env, \name) \evalarrow \envp
+    \removelocal(\env, \name) \evalarrow \newenv
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Reading an Identifier}
-
+\section{SemanticsRule.ReadIdentifier \label{sec:SemanticsRule.ReadIdentifier}}
+\subsection{Prose}
 The relation
 \[
   \readidentifier(\overname{\identifier}{\name}\aslsep\overname{\vals}{\vv}) \;\aslrel\; (\overname{\vals}{\vv} \times \XGraphs)
 \]
-represents reading a value $\vv$ into a storage element given by an identifier $\name$.
-The result is the value and a graph containing a single Read Effect denoting
-reading $\vv$ into $\name$.
+reads a value $\vv$ into a storage element given by an identifier $\name$.
+The result is the value and an execution graph containing a single Read Effect,
+which denoting reading from $\name$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[read\_identifier]{}
+  \inferrule{}
   {
     \readidentifier(\name, \vv) \evalarrow (\vv, \ReadEffect(\name))
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Writing to an Identifier}
-
+\section{SemanticsRule.WriteIdentifier \label{sec:SemanticsRule.WriteIdentifier}}
+\subsection{Prose}
 The relation
 \[
-  \writeidentifier(\overname{\identifier}{\name}\aslsep\overname{\vals}{\vv}) \;\aslrel\; (\overname{\vals}{\vv} \times \XGraphs)
+  \writeidentifier(\overname{\identifier}{\name}\aslsep\overname{\vals}{\vv}) \;\aslrel\; \XGraphs
 \]
-represents reading a value $\vv$ into a storage element given by an identifier $\name$.
-The result is the value and a graph containing a single Read Effect denoting
-reading $\vv$ into $\name$.
+writes the value $\vv$ into a storage element given by an identifier $\name$.
+The result is an execution graph containing a single Write Effect,
+which denotes writing into $\name$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[write\_identifier]{}
+  \inferrule{}
   {
     \writeidentifier(\name, \vv) \evalarrow \WriteEffect(\name)
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Creating a Bitvector}
+\section{SemanticsRule.CreateBitvector \label{sec:SemanticsRule.CreateBitvector}}
+\subsection{Prose}
 The relation
 \[
   \createbitvector(\overname{\vals^*}{\vvs}) \;\aslrel\; \tbitvector
 \]
-creates a native vector value from a sequence of values.
+creates a native vector value bitvector from a sequence of values $\vvs$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[create\_vector]{}
+  \inferrule{}
   {
     \createbitvector(\vvs) \evalarrow \nvbitvector{\vvs}
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Concatenating Bitvectors}
+\section{SemanticsRule.ConcatBitvectors \label{sec:SemanticsRule.ConcatBitvectors}}
+\subsection{Prose}
 The relation
 \[
   \concatbitvectors(\overname{\tbitvector^*}{\vvs}) \;\aslrel\; \tbitvector
 \]
-transforms a, possibly empty, list of bitvector native values into a single bitvector.
+transforms a, possibly empty, list of bitvector native values $\vvs$ into a single bitvector.
 
+\begin{emptyformal}
+\subsection{Formally}
 (Recall that $\epsilon$ stands for an empty sequence and $\cdot$ concatenates sequences.)
 \begin{mathpar}
-  \inferrule[concat\_bitvectors\_empty]{}
+  \inferrule[ConcatBitvector.Empty]{}
   {
     \concatbitvectors(\emptylist) \evalarrow \nvbitvector(\epsilon)
   }
   \and
-  \inferrule[concat\_bitvectors\_non\_empty]{
+  \inferrule[ConcatBitvector.NonEmpty]{
     \vvs \eqname [\vv] + \vvs'\\
     \vv\eqname\nvbitvector(\bv)\\
     \concatbitvectors(\vvs') \evalarrow \nvbitvector(\bv')\\
@@ -1128,15 +1206,33 @@ \section{Concatenating Bitvectors}
     \concatbitvectors(\vvs) \evalarrow \nvbitvector(\vres)
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Reading from a Bitvector}
+\section{SemanticsRule.ReadFromBitvector \label{sec:SemanticsRule.ReadFromBitvector}}
+\subsection{Prose}
+The relation
+\[
+  \readfrombitvector(\overname{\tbitvector}{\bv} \aslsep \overname{(\tint\times\tint)^*}{\slices}) \;\aslrel\;
+  \overname{\tbitvector}{\vv} \cup \overname{\TError}{\ErrorConfig}
+\]
+reads from a bitvector $\bv$, or an integer seen as a bitvector, the indices specified by the list of slices $\slices$,
+thereby concatenating their values,
+and one of the following apply:
+\begin{itemize}
+  \item all indices are in range for $\bv$ and the returned bitvector consists of the concatenated bits specified
+  by the slices.
+  \item there exists an out-of-range index and an error is returned.
+\end{itemize}
+
+\begin{emptyformal}
+\subsection{Formally}
 We start by introducing a few helper relations.
 
 \newcommand\positioninrange[0]{\texttt{position\_in\_range}}
 The predicate $\positioninrange(\vs, \vl, n)$ checks whether the indices starting at index $\vs$ and
 up to $\vs + \vl$, inclusive, would refer to actual indices of a bitvector of length $n$:
 \begin{mathpar}
-  \inferrule[position\_in\_range]{
+  \inferrule[PositionInRange]{
     \vs \geq 0\\
     \vl \geq 0\\
     \vs + \vl < \vn
@@ -1155,15 +1251,15 @@ \section{Reading from a Bitvector}
 unless an index would be out of range for a bitvector of length $\vn$, in which case it returns an error configuration.
 
 \begin{mathpar}
-  \inferrule[slices\_to\_positions\_out\_of\_range]{
+  \inferrule[SlicesToPositionsOutOfRange]{
     \slices \eqname [i=1..k: (\nvint(\vs_i), \nvint(\vl_i))]\\
     j \in 1..k: \neg\positioninrange(\vs_j, \vl_j, \vn)
   }
   {
-    \slicestopositions(\vn, \slices) \evalarrow \Error(\texttt{"Slice position out of range"})
+    \slicestopositions(\vn, \slices) \evalarrow \ErrorVal{Slice\_PositionOutOfRange}
   }
   \and
-  \inferrule[slices\_to\_positions\_in\_range]{
+  \inferrule[SlicesToPositionsInRange]{
     \slices \eqname [i=1..k: (\nvint(\vs_i), \nvint(\vl_i))]\\
     i=1..k: \positioninrange(\vs_i, \vl_i, \vn)\\
     \positions = [\vs_1,\ldots,\vs_1+\vl_1] + \ldots + [\vs_k,\ldots,\vs_k+\vl_k]\\
@@ -1176,12 +1272,12 @@ \section{Reading from a Bitvector}
 The function $\asbitvector : (\tbitvector\cup\tint) \rightarrow \{0,1\}^*$ transforms native value integers and native value bitvectors into
 a sequence of binary values:
 \begin{mathpar}
-  \inferrule[as\_bitvector\_bitvector]{}
+  \inferrule[AsBitvectorBitvector]{}
   {
     \asbitvector(\nvbitvector(\bv)) \evalarrow \bv
   }
   \and
-  \inferrule[as\_bitvector\_int]{
+  \inferrule[AsBitvectorInt]{
     \bv = \text{ two's complement representation of }n
   }
   {
@@ -1189,24 +1285,14 @@ \section{Reading from a Bitvector}
   }
 \end{mathpar}
 
-Finally, the relation
-\[
-  \readfrombitvector(\overname{\tbitvector}{\bv} \aslsep \overname{(\tint\times\tint)^*}{\slices}) \;\aslrel\;
-  \overname{\tbitvector}{\vv} \cup \overname{\TError}{\ErrorConfig}
-\]
-reads from a bitvector $\bv$, or an integer seen as a bitvector, the indices specified by the list of slices $\slices$.
-If all indices are in range for $\bv$, then the returned bitvector consists of the concatenated bits specified
-by the slices.
-Otherwise, an error configuration is returned.
-%
-The rules below distinguish between empty bitvectors and non-empty bitvectors.
+Finally, the rules below distinguish between empty bitvectors and non-empty bitvectors.
 \begin{mathpar}
-  \inferrule[read\_from\_bitvector\_empty]{}
+  \inferrule[ReadFromBitvector.Empty]{}
   {
     \readfrombitvector(\bv, \emptylist) \evalarrow \nvbitvector(\epsilon)
   }
   \and
-  \inferrule[read\_from\_bitvector\_non\_empty]{
+  \inferrule[ReadFromBitvector.NonEmpty]{
     \asbitvector(\bv) = \vb_n \ldots \vb_1\\
     \slicestopositions(n, \slices) \evalarrow [j_{1..m}] \terminateas \ErrorConfig\\
     \vv = \nvbitvector(\vb_{j_m + 1}\ldots\vb_{j_1 + 1})
@@ -1217,24 +1303,36 @@ \section{Reading from a Bitvector}
 \end{mathpar}
 Notice that the bits of a bitvector go from the least significant bit being on the right to the most significant bit being on the left,
 which is reflected by how the rules list the bits.
+The effect of placing the bits in sequence is that of concatenating the results
+from all of the given slices.
 Also notice that bitvector bits are numbered from 1 and on, which is why we add 1 to the indices specified
 by the slices when accessing a bit.
+\end{emptyformal}
 
-\section{Writing to a Bitvector}
+\section{SemanticsRule.WriteToBitvector \label{sec:SemanticsRule.WriteToBitvector}}
+\subsection{Prose}
 The relation
 \[
   \writetobitvector(\overname{(\tint\times\tint)^*}{\slices} \aslsep \overname{\tbitvector}{\src} \aslsep \overname{\tbitvector}{\dst})
   \;\bigtimes\; \overname{\tbitvector}{\vv} \cup \overname{\TError}{\ErrorConfig}
 \]
-overwrites the bits of $\dst$ at the positions given by $\slices$ with the bits of $\src$.
+overwrites the bits of $\dst$ at the positions given by $\slices$ with the bits of $\src$
+and one of the following apply:
+\begin{itemize}
+  \item all positions specified by $\slices$ are within range for $\dst$ and the modified version
+  of $\dst$ with the bits of $\src$ at the specified positions is returned;
+  \item there exists a position in $\slices$ that is not in range for $\dst$ and an error is returned.
+\end{itemize}
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[write\_to\_bitvector\_empty]{}
+  \inferrule[WriteToBitvector.Empty]{}
   {
     \writetobitvector(\emptylist, \nvbitvector(\epsilon), \nvbitvector(\epsilon)) \evalarrow \nvbitvector(\epsilon)
   }
   \and
-  \inferrule[write\_to\_bitvector\_non\_empty]{
+  \inferrule[WriteToBitvector.NonEmpty]{
     \asbitvector(\src) = \vs_n \ldots \vs_1\\
     \asbitvector(\dst) = \vd_n \ldots \vd_1\\
     \slicestopositions(n, \slices) \evalarrow \positions \terminateas \ErrorConfig\\
@@ -1248,16 +1346,20 @@ \section{Writing to a Bitvector}
     \writetobitvector(\slices, \src, \dst) \evalarrow \vv
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Reading from a Vector}
+\section{SemanticsRule.GetIndex \label{sec:SemanticsRule.GetIndex}}
+\subsection{Prose}
 The relation
 \[
   \getindex(\overname{\N}{\vi} \aslsep \overname{\tvector}{\vvec}) \;\aslrel\; \overname{\tvector}{\vv_{\vi}}
 \]
 reads the value $\vv_i$ from the vector of values $\vvec$ at the index $\vi$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[get\_index]{
+  \inferrule{
     \vvec \eqname [\vv_{i=0..k}]\\
     \vi \leq k\\
   }
@@ -1275,16 +1377,20 @@ \section{Reading from a Vector}
   involved and the corresponding lists of expressions.
 \end{itemize}
 If the rules listed above do not hold the type checker fails.
+\end{emptyformal}
 
-\section{Writing to a Vector}
+\section{SemanticsRule.SetIndex \label{sec:SemanticsRule.SetIndex}}
+\subsection{Prose}
 The relation
 \[
   \setindex(\overname{\N}{\vi} \aslsep \overname{\vals}{\vv} \aslsep \overname{\tvector}{\vvec}) \;\aslrel\; \overname{\tvector}{\vres}
 \]
 overwrites the value at the given index $\vi$ in a vector of values $\vvec$ with the new value $\vv$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[set\_index]{
+  \inferrule{
     \vvec \eqname [\vu_{0..k}]\\
     \vi \leq k\\
     \vres \eqname [\vw_{0..k}]\\
@@ -1296,16 +1402,20 @@ \section{Writing to a Vector}
   }
 \end{mathpar}
 Similar to $\getindex$, there is no need to handle the out-of-range index case.
+\end{emptyformal}
 
-\section{Reading a Field}
+\section{SemanticsRule.GetField \label{sec:SemanticsRule.GetField}}
+\subsection{Prose}
 The relation
 \[
   \getfield(\overname{\identifier}{\name} \aslsep \overname{\trecord}{\record}) \;\aslrel\; \vals
 \]
 retrieves the value corresponding to the field name $\name$ from the record value $\record$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[get\_field]{
+  \inferrule{
     \record \eqname \nvrecord{\fieldmap}
   }
   {
@@ -1313,16 +1423,20 @@ \section{Reading a Field}
   }
 \end{mathpar}
 The type-checker ensures, via TypingRule.EGetRecordField, that the field $\name$ exists in $\record$.
+\end{emptyformal}
 
-\section{Writing a Field}
+\section{SemanticsRule.SetField \label{sec:SemanticsRule.SetField}}
+\subsection{Prose}
 The relation
 \[
   \setfield(\overname{\identifier}{\name} \aslsep \overname{\vals}{\vv} \aslsep \overname{\trecord}{\record}) \;\aslrel\; \trecord
 \]
 overwrites the value corresponding to the field name $\name$ in the record value $\record$ with the value $\vv$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[set\_field]{
+  \inferrule{
     \record \eqname \nvrecord{\fieldmap}\\
     \fieldmap' = \fieldmap[\name\mapsto\vv]
   }
@@ -1331,94 +1445,124 @@ \section{Writing a Field}
   }
 \end{mathpar}
 The type-checker ensures that the field $\name$ exists in $\record$.
+\end{emptyformal}
 
-\section{Declaring a Local Identifier}
+\section{SemanticsRule.DeclareLocalIdentifier \label{sec:SemanticsRule.DeclareLocalIdentifier}}
+\subsection{Prose}
 The relation
 \[
   \declarelocalidentifier(\overname{\envs}{\env} \aslsep \overname{\identifier}{\name} \aslsep \overname{\vals}{\vv}) \;\aslrel\;
-  (\overname{\envs}{\envp}\times\overname{\XGraphs}{\vg})
+  (\overname{\envs}{\newenv}\times\overname{\XGraphs}{\vg})
 \]
 associates $\vv$ to $\name$ as a local storage element in the environment $\env$ and
-returns the updated environment $\envp$ with the execution graph that consists of a Write Effect to $\name$.
+returns the updated environment $\newenv$ with the execution graph that consists of a Write Effect to $\name$.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[declare\_local\_identifier]{
+  \inferrule{
     \vg = \WriteEffect(\name)\\
     \env \eqname (\tenv, (G^\denv, L^\denv))\\
-    \envp = (\tenv, (G^\denv, L^\denv[\name\mapsto \vv]))
+    \newenv = (\tenv, (G^\denv, L^\denv[\name\mapsto \vv]))
   }
-  { \declarelocalidentifier(\env, \name, \vv) \evalarrow (\envp, \vg)  }
+  { \declarelocalidentifier(\env, \name, \vv) \evalarrow (\newenv, \vg)  }
 \end{mathpar}
+\end{emptyformal}
 
+\section{SemanticsRule.DeclareLocalIdentifierM \label{sec:SemanticsRule.DeclareLocalIdentifierM}}
+\subsection{Prose}
 The relation
 \[
   \declarelocalidentifierm(\overname{\envs}{\env} \aslsep
    \overname{\identifier}{\vx} \aslsep
    \overname{(\overname{\vals}{\vv}\times\overname{\XGraphs}{\vg})}{\vm}) \;\aslrel\;
-  (\overname{\envs}{\envp} \times \overname{\XGraphs}{\vgtwo})
+  (\overname{\envs}{\newenv} \times \overname{\XGraphs}{\vgtwo})
 \]
-declares the local identifier $\vx$ in the environment $\env$ and composes it using
-a data label with the graph $\vg$:
+declares the local identifier $\vx$ in the environment $\env$, in the context
+of the value-graph pair $(\vv, \vg)$, and all of the following apply:
+\begin{itemize}
+  \item \newenv\ is the environment $\env$ modified to declare the variable $\vx$ as a local storage element;
+  \item $\vgone$ is the execution graph resulting from the declaration of $\vx$;
+  \item $\vgtwo$ is the execution graph resulting from the ordered composition of $\vg$ and $\vgone$
+  with the data label.
+\end{itemize}
+
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[declare\_local\_identifier\_m]{
+  \inferrule{
     \vm \eqname (\vv, \vg)\\
-    \declarelocalidentifier(\env, \vx, \vv) \evalarrow (\envp, \vgp)\\
-    \vgtwo = \ordered{\vg}{\asldata}{\vgp}
+    \declarelocalidentifier(\env, \vx, \vv) \evalarrow (\newenv, \vgone)\\
+    \vgtwo = \ordered{\vg}{\asldata}{\vgone}
   }
   {
-    \declarelocalidentifierm(\env, \vx, \vm) \evalarrow (\envp, \vgtwo)
+    \declarelocalidentifierm(\env, \vx, \vm) \evalarrow (\newenv, \vgtwo)
   }
 \end{mathpar}
+\end{emptyformal}
 
+\section{SemanticsRule.DeclareLocalIdentifierMM \label{sec:SemanticsRule.DeclareLocalIdentifierMM}}
+\subsection{Prose}
 The relation
 \[
   \declarelocalidentifiermm(\overname{\envs}{\env} \aslsep
    \overname{\identifier}{\vx} \aslsep
    \overname{(\overname{\vals}{\vv}\times\overname{\XGraphs}{\vg})}{\vm}) \;\aslrel\;
-  (\overname{\envs}{\envp} \times \overname{\XGraphs}{\vgtwo})
+  (\overname{\envs}{\newenv} \times \overname{\XGraphs}{\vgtwo})
 \]
-declares the local identifier $\vx$ in the environment $\env$ and composes it using
-a program order label with the graph $\vg$:
+declares the local identifier $\vx$ in the environment $\env$,
+in the context of the value-graph pair $(\vv, \vg)$,
+and all of the following apply:
+\begin{itemize}
+  \item \newenv\ is the environment $\env$ modified to declare the variable $\vx$ as a local storage element;
+  \item $\vgone$ is the execution graph resulting from the declaration of $\vx$;
+  \item $\vgtwo$ is the execution graph resulting from the ordered composition of $\vg$ and $\vgone$
+  with the program order label.
+\end{itemize}
+
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[declare\_local\_identifier\_mm]{
+  \inferrule{
     \vm \eqname (\vv, \vg)\\
-    \declarelocalidentifierm(\env, \vx, \vv) \evalarrow (\envp, \vgp)\\
-    \vgtwo = \ordered{\vg}{\aslpo}{\vgp}
+    \declarelocalidentifierm(\env, \vx, \vv) \evalarrow (\newenv, \vgone)\\
+    \vgtwo = \ordered{\vg}{\aslpo}{\vgone}
   }
   {
-    \declarelocalidentifiermm(\env, \vx, \vm) \evalarrow (\envp, \vgtwo)
+    \declarelocalidentifiermm(\env, \vx, \vm) \evalarrow (\newenv, \vgtwo)
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Declaring a Global Identifier}
+\section{SemanticsRule.DeclareGlobal \label{sec:SemanticsRule.DeclareGlobal}}
+\subsection{Prose}
 The relation
 \[
-  \declareglobal(\overname{\identifier}{\name} \aslsep \overname{\vals}{\vv} \aslsep \overname{\envs}{\env}) \;\aslrel\; \overname{\envs}{\envp}
+  \declareglobal(\overname{\identifier}{\name} \aslsep \overname{\vals}{\vv} \aslsep \overname{\envs}{\env}) \;\aslrel\; \overname{\envs}{\newenv}
 \]
 updates the environment $\env$ by mapping $\name$ to $\vv$ as a global storage element.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule[declare\_global]{
+  \inferrule{
     \env \eqname (\tenv, (G^\denv, L^\denv))\\
-    \envp = (\tenv, (G^\denv[\name\mapsto \vv], L^\denv))
+    \newenv = (\tenv, (G^\denv[\name\mapsto \vv], L^\denv))
   }
-  { \declareglobal(\name, \vv, \env) \evalarrow \envp  }
+  { \declareglobal(\name, \vv, \env) \evalarrow \newenv  }
 \end{mathpar}
+\end{emptyformal}
 
-
-\section{Obtaining the Base Value of a Type \label{sec:basevalue}}
+\section{SemanticsRule.BaseValue \label{sec:SemanticsRule.BaseValue}}
+\subsection{Prose}
 The relation
 \[
   \basevalue(\overname{\envs}{\env} \aslsep \overname{\ty}{\vt}) \;\aslrel\;
   (\overname{\vals}{\vv} \times \overname{\XGraphs}{\vg}) \cup \overname{\TError}{\ErrorConfig}
 \]
-returns the \emph{base value} $\vv$ of the type $\vt$ in the environment $\env$, as well as the execution graph $\vg$ that results
-from evaluating any of the side-effect-free expressions appearing in $\vt$.
-%
-Evaluating those inner expressions is done via the relation $\texttt{eval\_expr\_sef}$~\ref{sec:SemanticsRule.ESideEffectFreeExpr}.
-If evaluating an inner expression results in an error, there is no base value and an error configuration is returned.
+attempts to return the \emph{base value} of a type.
 
-To obtain the base value of a type, we first obtain its \emph{structure}, using the function
+\paragraph{Type Structure} To obtain the base value of a type, we first obtain its \emph{structure}, using the function
 $\tstruct : \ty \partialto \ty$.
 The structure of a type is the type that can hold the same set of values, but does not itself
 contain any other type names.
@@ -1428,26 +1572,137 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 %
 Since we assume the specification is well-typed (\secref{MeaningfulASLSpecifications}), $\tstruct$ always returns a valid type.
 
+The base value of the type $\vt$ in the environment $\env$ is $\vv$,
+as well as the execution graph $\vg$ that results
+from evaluating any of the side-effect-free expressions appearing in $\vt$,
+or an error, and one of the following apply:
+\begin{itemize}
+  \item all of the following apply (\textsc{boolean}):
+  \begin{itemize}
+    \item the structure of $\vt$ is the Boolean type;
+    \item $\vv$ is the native Boolean "true" value;
+    \item $\vg$ is the empty graph.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{real}):
+  \begin{itemize}
+    \item the structure of $\vt$ is the real type;
+    \item $\vv$ is the native real value $0$;
+    \item $\vg$ is the empty graph.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{string}):
+  \begin{itemize}
+    \item the structure of $\vt$ is the string type;
+    \item $\vv$ is the native value for the empty string;
+    \item $\vg$ is the empty graph.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{bitvector}):
+  \begin{itemize}
+    \item the structure of $\vt$ is the bitvector with the length expression $\ve$;;
+    \item evaluating the side-effect-free expression $\ve$ results in the native value $\length$
+    and execution graph $\vg$,
+    or an error is returned, short-circuiting the entire rule;
+    \item $\vv$ is the bitvector of length $\length$ where all bits are $0$.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{enum}):
+  \begin{itemize}
+    \item the structure of $\vt$ is the enumeration type where the first identifier is $\id_1$;
+    \item $\vl$ is the literal associated with $\id_1$ in the static environment;
+    \item $\vv$ is the native value literal for $\vl$;
+    \item $\vg$ is the empty graph.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{unconstrained\_integer}):
+  \begin{itemize}
+    \item the structure of $\vt$ is that of the unconstrained integer;
+    \item $\vv$ is the native value integer $0$;
+    \item $\vg$ is the empty graph.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{well\_constrained\_integer}):
+  \begin{itemize}
+    \item the structure of $\vt$ is that of the well-constrained integer where the first constraint
+    is exact with the expression $\ve$;
+    \item $(\vv, \vg)$ is the result of evaluating the side-effect-free expression $\ve$.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{record}):
+  \begin{itemize}
+    \item the structure of $\vt$ is that of a record or an exception;
+    \item the base value of each field is obtained, and if any of the base values results in an error
+    then the entire rule short-circuits with that error;
+    \item $\vv$ is the native value record where each identifier in the record is mapped to its
+    respecive base value;
+    \item $\vg$ is the parallel composition of the graphs resulting from the base value evaluation
+    of all the fields.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{tuple}):
+  \begin{itemize}
+    \item the structure of $\vt$ is that of a tuple of types;
+    \item the base value of each type in the tuple is obtained, and if any of the base values results in an error
+    then the entire rule short-circuits with that error;
+    \item $\vv$ is the native value vector consists of the base values in the order of the corresponding types
+    of the tuple;
+    \item $\vg$ is the parallel composition of the graphs resulting from the base value evaluation
+    of all the tuple types.
+  \end{itemize}
+
+  \item all of the following apply (\textsc{array\_length\_global\_constant}):
+  \begin{itemize}
+    \item the structure of $\vt$ is that of an array with length expression $\elength$ and element type $\vvty$;
+    \item $\elength$ is the value of a declared constant;
+    \item $\elength$ is a variable expression with the variable name $\vx$;
+    \item the constant value for $\vx$ in the static environment is the literal integer for $n$;
+    \item either the base value of $\vvty$ in $\env$ is $(\velem, \vg)$ or an error, which short-circuits
+    the entire evaluation;
+    \item $\vv$ is the native value vector of length $n$ where each element is $\velem$;
+  \end{itemize}
+
+  \item all of the following apply (\textsc{array\_length\_expression}):
+  \begin{itemize}
+    \item the structure of $\vt$ is that of an array with length expression $\elength$ and element type $\vvty$;
+    \item $\elength$ is not the value of a declared constant;
+    \item either the base value of $\vvty$ in $\env$ is $(\velem, \vg)$ or an error, which short-circuits
+    the entire evaluation;
+    \item either evaluating the side-effect-free expression $\elength$ in the environment $\env$
+    results in $(\vlength, \vgtwo)$ or an error, which short-circuits
+    the entire evaluation;
+    \item $\vlength$ is the native value integer for $n$;
+    \item $\vv$ is the native value vector of length $n$ where each element is $\velem$;
+    \item $\vg$ is the ordered composition of $\vgone$ and $\vgtwo$ with the data label.
+  \end{itemize}
+\end{itemize}
+
+\begin{emptyformal}
+\subsection{Formally}
+Evaluating the inner expressions of the type $\vt$ is done via the relation\\
+$\texttt{eval\_expr\_sef}$~\ref{sec:SemanticsRule.ESideEffectFreeExpr}.
+If evaluating an inner expression results in an error, there is no base value and an error configuration is returned.
+
 \begin{mathpar}
-  \inferrule[base\_value\_bool]{
+  \inferrule[bool]{
     \tstruct(\vt) \eqname \TBool
   }
   {
-    \basevalue(\env, \vt) \evalarrow \nvbool(\True)
+    \basevalue(\env, \vt) \evalarrow (\nvbool(\True), \emptygraph)
   }
   \and
-  \inferrule[base\_value\_real]{
+  \inferrule[real]{
     \tstruct(\vt) \eqname \TReal
   }
   {
-    \basevalue(\env, \vt) \evalarrow \nvreal(0)
+    \basevalue(\env, \vt) \evalarrow (\nvreal(0), \emptygraph)
   }
   \and
-  \inferrule[base\_value\_string]{
+  \inferrule[string]{
     \tstruct(\vt) \eqname \TString
   }
   {
-    \basevalue(\env, \vt) \evalarrow \nvliteral{\lstring(\epsilon)}
+    \basevalue(\env, \vt) \evalarrow (\nvliteral{\lstring(\epsilon)}, \emptygraph)
   }
 \end{mathpar}
 
@@ -1455,12 +1710,12 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 of the length specified by the type (\ve). If the length is $0$, the bitvector consists of an
 empty sequence:
 \begin{mathpar}
-  \inferrule[base\_value\_bitvector]{
+  \inferrule[bitvector]{
     \tstruct(\vt) \eqname \TBits(\ve, \Ignore)\\
-    \evalexprsef{\env, \ve} \evalarrow (\nvint(\length), \emptygraph) \terminateas \ErrorConfig
+    \evalexprsef{\env, \ve} \evalarrow (\nvint(\length), \vg) \terminateas \ErrorConfig
   }
   {
-    \basevalue(\env, \vt) \evalarrow \nvbitvector(\overbrace{0\ldots 0}^{\length})
+    \basevalue(\env, \vt) \evalarrow (\nvbitvector(\overbrace{0\ldots 0}^{\length}), \vg)
   }
 \end{mathpar}
 
@@ -1468,11 +1723,11 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 Accessing this literal is done via the \constantsvalues\ map in the
 global component of the static environment:
 \begin{mathpar}
-  \inferrule[base\_value\_enum]{
+  \inferrule[enum]{
     \tstruct(\vt) \eqname \TEnum(\id_{1..k})\\
     \env \eqname (\tenv, \denv)\\
     \tenv \eqname (G^\tenv, L^\tenv)\\
-    G^\tenv.\constantsvalues(\id_1) = \vl
+    G^\tenv.\constantsvalues~(\id_1) = \vl
   }
   {
     \basevalue(\env, \vt) \evalarrow (\nvliteral{\vl}, \emptygraph)
@@ -1480,14 +1735,14 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 \end{mathpar}
 
 \begin{mathpar}
-  \inferrule[base\_value\_integer\_unconstrained]{
+  \inferrule[integer\_unconstrained]{
     \tstruct(\vt) \eqname \TInt(\unconstrained)
   }
   {
     \basevalue(\env, \vt) \evalarrow (\nvint(0), \emptygraph)
   }
   \and
-  \inferrule[base\_value\_integer\_constraint\_exact]{
+  \inferrule[integer\_constraint\_exact]{
     \tstruct(\vt) \eqname \TInt(\wellconstrained([\constraintexact(\ve)] + \Ignore))\\
     \evalexprsef{\env, \ve} \evalarrow C
   }
@@ -1496,7 +1751,7 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
   }
   \and
   \and
-  \inferrule[base\_value\_integer\_constraint\_range]{
+  \inferrule[integer\_constraint\_range]{
     \tstruct(\vt) \eqname \TInt(\wellconstrained([\constraintrange(\ve, \Ignore)] + \Ignore))\\
     \evalexprsef{\env, \ve} \evalarrow C
   }
@@ -1506,7 +1761,7 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 \end{mathpar}
 
 \begin{mathpar}
-  \inferrule[base\_value\_record]{
+  \inferrule[record]{
     \tstruct(\vt) \eqname L([i=1..k: (\id_i, \vt_i)])\\
     L \in \{\TRecord, \TException\}\\
     i=1..k: \basevalue(\env, \vt_i) \evalarrow (\vv_i, \vg_i) \terminateas \ErrorConfig\\
@@ -1519,7 +1774,7 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 \end{mathpar}
 
 \begin{mathpar}
-  \inferrule[base\_value\_tuple]{
+  \inferrule[tuple]{
     \tstruct(\vt) \eqname \TTuple([i=1..k: \vt_i])\\
     i=1..k: \basevalue(\env, \vt_i) \evalarrow (\vv_i, \vg_i) \terminateas \ErrorConfig\\
     \vv = \nvvector{\vv_{1..k}}\\
@@ -1534,7 +1789,7 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 The predicate $\isconstant$ checks whether the expression $\ve$ is a variable
 declared as a constant.
 \begin{mathpar}
-  \inferrule{
+  \inferrule[IsConstant]{
     \ve=\texttt{E\_Var}(\vx)\\
     \env \eqname (\tenv, \denv)\\
     \tenv \eqname (G^\tenv, L^\tenv)\\
@@ -1546,7 +1801,7 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
 \end{mathpar}
 
 \begin{mathpar}
-  \inferrule[base\_value\_array\_length\_global\_constant]{
+  \inferrule[array\_length\_global\_constant]{
     \tstruct(\vt) \eqname \TArray(\elength, \vvty)\\
     \basevalue(\env, \vvty) \evalarrow (\velem, \vg) \terminateas \ErrorConfig\\
     \isconstant(\elength)\\
@@ -1560,7 +1815,7 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
     \basevalue(\env, \vt) \evalarrow (\vv, \vg)
   }
   \and
-  \inferrule[base\_value\_array\_length\_expression]{
+  \inferrule[array\_length\_expression]{
     \tstruct(\vt) \eqname \TArray(\elength, \vvty)\\
     \basevalue(\env, \vvty) \evalarrow (\velem, \vgone) \terminateas \ErrorConfig\\
     \neg\isconstant(\elength)\\
@@ -1573,95 +1828,124 @@ \section{Obtaining the Base Value of a Type \label{sec:basevalue}}
     \basevalue(\env, \vt) \evalarrow (\vv, \vg)
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Checking Whether a Value Matches a Type}
+\section{SemanticsRule.IsValOfType}
 \subsection{Prose}
 The relation
 \[
   \isvaloftype(\overname{\envs}{\env} \aslsep \overname{\vals}{\vv} \aslsep \overname{\ty}{\vt}) \;\aslrel\;
   (\overname{\{\True,\False\}}{\vb} \times \overname{\XGraphs}{\vg}) \cup \overname{\TError}{\ErrorConfig}
 \]
-checks whether the value $\vv$ can be stored in a variable of type $\vt$ in the environment $\env$ and
-one of the following applies:
+checks whether the value $\vv$ can be stored in a variable of type $\vt$ in the environment $\env$,
+resulting in a Boolean value $\vb$ and execution graph $\vg$, \ProseOrError.
+
+This relation is used in the context of a checked type conversion,
+which means the type-checker rule TypingRule.CTC was already applied,
+thus filtering cases where the type inferred for the converted expression
+does not type-satisfy $\vt$. The semantics takes this into account and
+only returns \False\ in cases where dynamic information is required.
+
+One of the following applies:
 \begin{itemize}
-  \item Evaluation of all inner expressions in $\vt$ succeeds and the Boolean answer
-  along with the execution graph generated by evaluating any inner expressions of $\vt$.
-  \item Evaluation of an inner expression in $\vt$ fails and an error configuration is returned.
+  \item All of the following applies (\textsc{basic}):
+  \begin{itemize}
+    \item $\vt$ has the structure of a Boolean, a real, a string, or an enumeration;
+    \item $\vb$ is \True;
+    \item $\vg$ is the empty graph.
+  \end{itemize}
+
+  \item All of the following applies (\textsc{int\_unconstrained}):
+  \begin{itemize}
+    \item $\vt$ has the structure of the unconstrained integer;
+    \item $\vb$ is \True;
+    \item $\vg$ is the empty graph.
+  \end{itemize}
+
+  \item All of the following applies (\textsc{int\_wellconstrained}):
+  \begin{itemize}
+    \item $\vt$ has the structure of a well-constrained integer with constraints $\vc_{1..k}$;
+    \item $\vv$ is the native value integer for $n$;
+    \item either the evaluation of every constraint $\vc_i$ with $n$ in environment $\env$
+    yields a Boolean value $\vb_i$ and an execution graph $\vg_i$,
+    or the evaluation of one of the constraints results in an error, which short-circuits the entire
+    evaluation;
+    \item $\vb$ is the Boolean disjunction of all Boolean values $\vb_i$, for $i=1..k$;
+    \item $\vg$ is the parallel composition of all execution graphs $\vg_i$, for $i=1..k$;
+  \end{itemize}
+
+  \item All of the following applies (\textsc{record}):
+  \begin{itemize}
+    \item $\vt$ has the structure of a record or an exception, with a list of field names
+    $\id_i$, for $i=1..k$, associated with types $\vt_i$, for $i=1..k$;
+    \item the value of every field $\id_i$ in $\vv$ is $\vu_i$, for $i=1..k$,
+    \item either the evaluation of $\isvaloftype$ for every value $\vu_i$
+    and corresponding type $\vt_i$, for $i=1..k$,
+    results in a Boolean $\vb_i$ and execution graph $\vg_i$,
+    or one of the evaluations results in an error,
+    which short-circuits the entire evaluation;
+    \item $\vb$ is the Boolean conjunction of all Boolean values $\vb_i$, for $i=1..k$;
+    \item $\vg$ is the parallel composition of all execution graphs $\vg_i$, for $i=1..k$;
+    of the constraints.
+  \end{itemize}
+
+  \item All of the following applies (\textsc{tuple}):
+  \begin{itemize}
+    \item $\vt$ has the structure of a tuple with types $\vt_i$, for $i=1..k$;
+    \item the value at every index $i=1..k$ of $\vv$ is $\vu_i$, for $i=1..k$,
+    \item either the evaluation of $\isvaloftype$ for every value $\vu_i$
+    and corresponding type $\vt_i$, for $i=1..k$,
+    results in a Boolean $\vb_i$ and execution graph $\vg_i$,
+    or one of the evaluations results in an error,
+    which short-circuits the entire evaluation;
+    \item $\vb$ is the Boolean conjunction of all Boolean values $\vb_i$, for $i=1..k$;
+    \item $\vg$ is the parallel composition of all execution graphs $\vg_i$, for $i=1..k$;
+    of the constraints.
+  \end{itemize}
+
+  \item All of the following applies (\textsc{array}):
+  \begin{itemize}
+    \item $\vt$ has the structure of an array with length expression $\vt$
+    and element type $\vtone$;
+    \item evaluating the side-effect-free expression $\ve$ in environment $\env$
+    results in the native value integer for $k$ and execution graph $\vg$;
+    \item obtaining the values at indices $i=1..k$ from $\vv$ result in $\vv_i$;
+    \item either evaluating $\isvaloftype$ for $\vv_i$ and $\vtone$, for $i=1..k$,
+    all result in Boolean values $\vb_i$ and execution graphs $\vg_i$,
+    or one of the evaluations returns an error,
+    which short-circuits the entire evaluation;
+    \item $\vb$ is the Boolean conjunction of all Boolean values $\vb_i$, for $i=1..k$;
+    \item $\vg$ is the parallel composition of all execution graphs $\vg_i$, for $i=1..k$;
+    of the constraints.
+  \end{itemize}
 \end{itemize}
-This relation is used in the context of a checked type conversion.
 
 % \subsection{Code}
 %   \VerbatimInput[firstline=\ValOfTypeBegin, lastline=\ValOfTypeEnd]{../Interpreter.ml}
 
-  \subsection{Formally}
-  \newcommand\tstructglobal[0]{\texttt{get\_global\_structure}}
-  The helper relation
-  \[
-    \tstructglobal(\overname{\envs}{\env} \aslsep \overname{\ty}{\vt}) \;\aslrel\; \overname{\ty}{\vt'}
-  \]
-  obtains the structure of the type (see \secref{basevalue} for a description of type structuers)
-  $\vt$ in a static environment obtained from $\env$ by substituting
-  the local static environment with an empty one.
+\begin{emptyformal}
+\subsection{Formally}
   \newcommand\Bool[1]{\textsf{Boolean}(#1)}
   In the following rules, we write $\Bool{p}$ to mean $\True$ when the condition $p$ holds and $\False$
   otherwise.
-
-  \begin{mathpar}
-    \inferrule{
-      \env \eqname (\tenv, \Ignore)\\
-      \tstruct((G^\tenv, \emptyfunc), \vt) = \vt'
-    }
-    {
-      \tstructglobal(\env, \vt) \evalarrow \vt'
-    }
-  \end{mathpar}
+  %
+  Also, $\astlabel(n)$ is the label of the AST node $n$.
 
 \begin{mathpar}
-  \inferrule[is\_val\_of\_type\_bool]{
-    \tstructglobal(\env, \vt) \evalarrow \TBool\\
-    \vb = \Bool{\vv \in \tbool}\\
+  \inferrule[Basic (bool, real, string, enum)]{
+    \astlabel(\tstruct(\env, \vt)) \in \{\TBool, \TReal, \TString, \TEnum\}\\
     \vg = \emptygraph
   }
   {
-    \isvaloftype(\env, \vv, \vt) \evalarrow (\vb, \vg)
-  }
-  \and
-  \inferrule[is\_val\_of\_type\_real]{
-    \tstructglobal(\env, \vt) \evalarrow \TReal\\
-    \vb = \Bool{\vv \in \treal}\\
-    \vg = \emptygraph
-  }
-  {
-    \isvaloftype(\env, \vv, \vt) \evalarrow (\vb, \vg)
+    \isvaloftype(\env, \vv, \vt) \evalarrow (\True, \vg)
   }
   \and
-  \inferrule[is\_val\_of\_type\_string]{
-    \tstructglobal(\env, \vt) \evalarrow \TString\\
-    \vb = \Bool{\vv \in \tstring}\\
+  \inferrule[int\_unconstrained]{
+    \tstruct(\env, \vt) = \TInt(\unconstrained)\\
     \vg = \emptygraph
   }
   {
-    \isvaloftype(\env, \vv, \vt) \evalarrow (\vb, \vg)
-  }
-  \and
-  \inferrule[is\_val\_of\_type\_enum]{
-    \tstructglobal(\env, \vt) \evalarrow \TEnum(\id_{0..k})\\
-    \vb = \Bool{\exists j \in 1..k.\ \vv = \nvint(j)}\\
-    \vg = \emptygraph
-  }
-  {
-    \isvaloftype(\env, \vv, \vt) \evalarrow (\vb, \vg)
-  }
-\end{mathpar}
-
-\begin{mathpar}
-  \inferrule[is\_val\_of\_type\_int\_unconstrained]{
-    \tstructglobal(\env, \vt) \evalarrow \TInt(\unconstrained)\\
-    \vb = \Bool{\vv \in \tint}\\
-    \vg = \emptygraph
-  }
-  {
-    \isvaloftype(\env, \vv, \vt) \evalarrow (\vb, \vg)
+    \isvaloftype(\env, \vv, \vt) \evalarrow (\True, \vg)
   }
 \end{mathpar}
 
@@ -1698,8 +1982,8 @@ \subsection{Prose}
 
 Finally, we can check whether an integer value satisfies any of the constraints:
 \begin{mathpar}
-  \inferrule[is\_val\_of\_type\_int\_wellconstrained]{
-    \tstructglobal(\env, \vt) \evalarrow \TInt(\wellconstrained(\vc_{1..k}))\\
+  \inferrule[int\_wellconstrained]{
+    \tstruct(\env, \vt) = \TInt(\wellconstrained(\vc_{1..k}))\\
     \vv = \nvint(n)\\
     i=1..k: \integerconstraintsatisfied(\env, \vc_i, n) \evalarrow (\vb_i, \vg_i) \terminateas \ErrorConfig\\
     \vb = \Bool{\bigvee_{i=1}^k \vb_i}\\
@@ -1711,8 +1995,9 @@ \subsection{Prose}
 \end{mathpar}
 
 \begin{mathpar}
-  \inferrule[is\_val\_of\_type\_record]{
-    \tstructglobal(\env, \vt) \evalarrow \TRecord(i=1..k: \id_i\mapsto \vt_i)\\
+  \inferrule[record]{
+    \tstruct(\env, \vt) = L(i=1..k: \id_i\mapsto \vt_i)\\
+    L \in \{\TRecord, \TException\}\\
     i=1..k: \getfield(\id_i, \vv) \evalarrow \vu_i\\
     i=1..k: \isvaloftype(\env, \vu_i, \vt_i) \evalarrow (\vb_i, \vg_i) \terminateas \ErrorConfig\\
     \vb = \Bool{ \bigwedge_{i=1}^k \vb_i }\\
@@ -1724,9 +2009,9 @@ \subsection{Prose}
 \end{mathpar}
 
 \begin{mathpar}
-  \inferrule[is\_val\_of\_type\_tuple]{
-    \tstructglobal(\env, \vt) \evalarrow \TTuple(i=1..k: \vt_i)\\
-    i=1..k: \getindex(i, \vv) \evalarrow \vu_i \terminateas \ErrorConfig\\
+  \inferrule[tuple]{
+    \tstruct(\env, \vt) = \TTuple(i=1..k: \vt_i)\\
+    i=1..k: \getindex(i, \vv) \evalarrow \vu_i \terminateas\\
     i=1..k: \isvaloftype(\env, \vu_i, \vt_i) \evalarrow (\vb_i, \vg_i) \terminateas \ErrorConfig\\
     \vb = \Bool{ \bigwedge_{i=1}^k \vb_i }\\
     \vg = \parallel_{i=1}^k \vg_i
@@ -1737,11 +2022,11 @@ \subsection{Prose}
 \end{mathpar}
 
 \begin{mathpar}
-  \inferrule[is\_val\_of\_type\_array]{
-    \tstructglobal(\env, \vt) \evalarrow \TArray(\ve, \vt')\\
-    \evalexprsef{\env, \ve} \evalarrow (\nvint(k), \vg) \terminateas \ErrorConfig\\
+  \inferrule[array]{
+    \tstruct(\env, \vt) = \TArray(\ve, \vtone)\\
+    \evalexprsef{\env, \ve} \evalarrow (\nvint(k), \vg)\\
     i=1..k: \getindex(i, \vv) \evalarrow \vv_i\\
-    i=1..k: \isvaloftype(\env, \vv_i, \vt') \evalarrow (\vb_i, \vg_i) \terminateas \ErrorConfig\\
+    i=1..k: \isvaloftype(\env, \vv_i, \vtone) \evalarrow (\vb_i, \vg_i) \terminateas \ErrorConfig\\
     \vb = \Bool{ \bigwedge_{i=1}^k \vb_i }\\
     \vg = \parallel_{i=1}^k \vg_i
   }
@@ -1751,18 +2036,19 @@ \subsection{Prose}
 \end{mathpar}
 
 Notice that these rules cover all types, including named types ($\TNamed$),
-since $\tstructglobal$ replaces named types by their type definitions.
+since $\tstruct$ replaces named types by their type definitions.
 %
 Underconstrained integers (integers with an empty set of constraints)
-cannot appear as a type, since ASL syntax does not allow to:
+cannot appear as a type, since ASL syntax does not allow the following:
 \begin{itemize}
-\item Declare an underconstrained integer as a variable,
-\item Declare an alias to an underconstrained integer type, and
-\item Declare an underconstrained integer in a compound type.
+\item Declaring an underconstrained integer as a variable,
+\item Declaring an alias to an underconstrained integer type, and
+\item Declaring an underconstrained integer in a compound type.
 \end{itemize}
+\end{emptyformal}
 
 \section{Applying a Unary Operator \label{sec:UnaryOperator}}
-
+\subsection{Prose}
 The relation
 \[
   \unop(\op \aslsep \vals) \;\aslrel\; \vals
@@ -1770,6 +2056,8 @@ \section{Applying a Unary Operator \label{sec:UnaryOperator}}
 evaluates an operator over a native value and returns the resulting
 native value.
 
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
   \inferrule[negate\_int]{}{
     \unop(\NEG, \nvint(n)) \evalarrow \nvint(- n)
@@ -1789,9 +2077,10 @@ \section{Applying a Unary Operator \label{sec:UnaryOperator}}
     \unop(\NOT, \nvbitvector(\bits)) \evalarrow \nvbitvector(c)
   }
 \end{mathpar}
+\end{emptyformal}
 
-\section{Applying a Binary Operator \label{sec:BinaryOperator}}
-
+\section{SemanticsRule.BinopOperator \label{sec:SemanticsRule.BinopOperator}}
+\subsection{Prose}
 The relation
 \[
   \binop(\op \aslsep \vals \aslsep \vals) \;\aslrel\; (\vals \cup \TError)
@@ -1800,8 +2089,10 @@ \section{Applying a Binary Operator \label{sec:BinaryOperator}}
 native value or an error, if it is considered illegal to apply the operator
 to the given values.
 
-\newcommand\ErrorDivDenominatorNegative[0]{\texttt{"DivDenominatorNegative"}}
-\subsection{Arithmetic Operators Over Integer Values \label{sec:AthimeticOverInt}}
+\begin{emptyformal}
+\subsection{Formally}
+
+\subsubsection{Arithmetic Operators Over Integer Values \label{sec:AthimeticOverInt}}
 \begin{mathpar}
   \inferrule[add\_int]{ n = a + b }{
     \binop(\PLUS, \nvint(a), \nvint(b)) \evalarrow \nvint(n)
@@ -1822,14 +2113,14 @@ \subsection{Arithmetic Operators Over Integer Values \label{sec:AthimeticOverInt
   }
   \and
   \inferrule[div\_int\_error\_denominator\_negative]{  b \leq 0 }{
-    \binop(\DIV, \nvint(a), \nvint(b)) \evalarrow \Error(\ErrorDivDenominatorNegative)
+    \binop(\DIV, \nvint(a), \nvint(b)) \evalarrow \ErrorVal{Div\_DenominatorNegative}
   }
   \and
   \inferrule[div\_int\_error\_indivisible]{  b > 0 \\
   n = a \div b \\
   n \not\in \Z
   }{
-    \binop(\DIV, \nvint(a), \nvint(b)) \evalarrow \Error(\texttt{"/ indivisibility error!"})
+    \binop(\DIV, \nvint(a), \nvint(b)) \evalarrow \ErrorVal{DIVInt\_Indivisibile}
   }
   \and
   \inferrule[fdiv\_int\_pos]{  b > 0 \\
@@ -1842,7 +2133,7 @@ \subsection{Arithmetic Operators Over Integer Values \label{sec:AthimeticOverInt
   n = -(\lceil (-a) \div b \rceil)
   }{ \binop(\DIVRM, \nvint(a), \nvint(b)) \evalarrow \nvint(n) }
   \and
-  \inferrule[fdiv\_int\_denominator\_negative]{  b \leq 0 }{ \binop(\DIVRM, \nvint(a), \nvint(b)) \evalarrow \Error(\texttt{"DIVRM denominator error!"}) }
+  \inferrule[fdiv\_int\_denominator\_negative]{  b \leq 0 }{ \binop(\DIVRM, \nvint(a), \nvint(b)) \evalarrow \ErrorVal{DIVRM\_DenominatorNegative} }
   \and
   \inferrule[frem\_int\_pos]{  b > 0 \\
     \binop(\DIVRM, \nvint(a), \nvint(b)) \evalarrow c \\
@@ -1850,7 +2141,7 @@ \subsection{Arithmetic Operators Over Integer Values \label{sec:AthimeticOverInt
   }{ \binop(\MOD, \nvint(a), \nvint(b)) \evalarrow \nvint(n) }
   \and
   \inferrule[frem\_int\_error\_denominator\_not\_positive]{  b \leq 0
-  }{ \binop(\MOD, \nvint(a), \nvint(b)) \evalarrow \Error(\texttt{"MOD denominator error!"}) }
+  }{ \binop(\MOD, \nvint(a), \nvint(b)) \evalarrow \ErrorVal{MOD\_DenominatorNotPositive} }
 \end{mathpar}
 
 \begin{mathpar}
@@ -1858,7 +2149,7 @@ \subsection{Arithmetic Operators Over Integer Values \label{sec:AthimeticOverInt
   }{ \binop(\POW, \nvint(a), \nvint(b)) \evalarrow \nvint(n)}
   \and
   \inferrule[exp\_int\_error]{  b < 0 \\ n = a^b
-  }{ \binop(\POW, \nvint(a), \nvint(b)) \evalarrow \Error(\texttt{"POW exponent error!"}) }
+  }{ \binop(\POW, \nvint(a), \nvint(b)) \evalarrow \ErrorVal{POW\_ExponentNegative} }
   \and
   \inferrule[shiftleft\_int]{  \binop(\MUL, \nvint(a), \binop(\POW, \nvint(2), \nvint(b))) \evalarrow C
   }{ \binop(\SHL, \nvint(a), \nvint(b)) \evalarrow C}
@@ -1867,7 +2158,7 @@ \subsection{Arithmetic Operators Over Integer Values \label{sec:AthimeticOverInt
   }{ \binop(\SHR, \nvint(a), \nvint(b)) \evalarrow C}
 \end{mathpar}
 
-\subsection{Relational Operators Over Integer Values \label{sec:RelationalOverInt}}
+\subsubsection{Relational Operators Over Integer Values \label{sec:RelationalOverInt}}
 \begin{mathpar}
   \inferrule[eq\_real]{  c=\Bool{a = b} }{ \binop(\EQOP, \nvint(a), \nvint(b)) \evalarrow \nvbool(c)}
   \and
@@ -1886,7 +2177,7 @@ \subsection{Relational Operators Over Integer Values \label{sec:RelationalOverIn
 employ the mathematical meaning of logical conjunction $\wedge$, logical disjunction $\vee$,
 and logical negation $\neg$, over the Boolean values $\True$ and $\False$.
 
-\subsection{Boolean Operators Over Boolean Values \label{sec:BooleanOverBoolean}}
+\subsubsection{Boolean Operators Over Boolean Values \label{sec:BooleanOverBoolean}}
 \begin{mathpar}
 \inferrule[and\_bool]{}{ \binop(\BAND, \nvbool(a), \nvbool(b)) \evalarrow \nvbool(a \wedge b)}
 \and
@@ -1903,7 +2194,7 @@ \subsection{Boolean Operators Over Boolean Values \label{sec:BooleanOverBoolean}
 }{ \binop(\NEQ, \nvbool(a), \nvbool(b)) \evalarrow \nvbool(c)}
 \end{mathpar}
 
-\subsection{Arithmetic Operators Over Real Values \label{sec:AthimeticOverReal}}
+\subsubsection{Arithmetic Operators Over Real Values \label{sec:AthimeticOverReal}}
 \begin{mathpar}
   \inferrule[add\_real]{}{\binop(\PLUS, \nvreal(a), \nvreal(b)) \evalarrow \nvreal(a+b)}
 \and
@@ -1913,12 +2204,12 @@ \subsection{Arithmetic Operators Over Real Values \label{sec:AthimeticOverReal}}
 \and
 \inferrule[div\_real]{b \neq 0}{\binop(\RDIV, \nvreal(a), \nvreal(b)) \evalarrow \nvreal(a\div b)}
 \and
-\inferrule[div\_real\_error]{b = 0}{\binop(\RDIV, \nvreal(a), \nvreal(b)) \evalarrow \Error(\texttt{"/ denominator is 0!})}
+\inferrule[div\_real\_error]{b = 0}{\binop(\RDIV, \nvreal(a), \nvreal(b)) \evalarrow \ErrorVal{RDIV\_DenominatorZero}}
 \and
 \inferrule[exp\_real]{b \geq 0}{\binop(\POW, \nvreal(a), \nvreal(b)) \evalarrow \nvreal(a^b)}
 \end{mathpar}
 
-\subsection{Relational Operators Over Real Values \label{sec:RealtionalOverReal}}
+\subsubsection{Relational Operators Over Real Values \label{sec:RealtionalOverReal}}
 \begin{mathpar}
   \inferrule[eq\_real]{  c=\Bool{a = b} }{ \binop(\EQOP, \nvreal(a), \nvreal(b)) \evalarrow \nvbool(c)}
   \and
@@ -2021,6 +2312,7 @@ \subsection{Operators Over Bitvectors \label{sec:BitvectorOperations}}
     \binop(\MINUS, \nvbitvector(a_{1..k}), \nvint(b)) \evalarrow \nvbitvector(c)
   }
 \end{mathpar}
+\end{emptyformal}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Evaluation of Expressions \label{chap:eval_expr}}
@@ -2032,10 +2324,12 @@ \chapter{Evaluation of Expressions \label{chap:eval_expr}}
             \Normal((\overname{\vals}{\vv} \times \overname{\XGraphs}{\vg}) \aslsep \overname{\envs}{\newenv}) \cup
             \overname{\TThrowing}{\ThrowingConfig} \cup \overname{\TError}{\ErrorConfig}
 \]
-evaluates the expression $\ve$ under environment $\env$.
-When the evaluation terminates normally it returns a native value $\vv$, a concurrent execution graph $\vg$,
-and a modified environment $\newenv$.
-Otherwise, the evaluation terminates abnormally.
+evaluates the expression $\ve$ under environment $\env$ and one of the following applies:
+\begin{itemize}
+  \item the evaluation terminates normally, returning a native value $\vv$, a concurrent execution graph $\vg$,
+  and a modified environment $\newenv$;
+  \item the evaluation terminates abnormally.
+\end{itemize}
 
 We start by defining the following helper relations:
 \begin{itemize}
@@ -2069,6 +2363,7 @@ \chapter{Evaluation of Expressions \label{chap:eval_expr}}
 \end{itemize}
 
 \section{SemanticsRule.EExprList \label{sec:SemanticsRule.EExprList}}
+\subsection{Prose}
 The relation
 \[
   \evalexprlist{\overname{\envs}{\env} \aslsep \overname{\expr^*}{\vle}} \;\aslrel\;
@@ -2079,17 +2374,20 @@ \section{SemanticsRule.EExprList \label{sec:SemanticsRule.EExprList}}
 and returns the resulting value $\vv$, the parallel composition of the execution graphs
 generated from evaluating each expression, and the new environment $\newenv$.
 If the evaluation of any expression terminates abnormally then the abnormal configuration is returned.
-(Recall that $+$ stands for list concatenation):
+
+\begin{emptyformal}
+\subsection{Formally}
+Recall that $+$ stands for list concatenation.
 \begin{mathpar}
-  \inferrule[eval\_expr\_list\_empty]{}
+  \inferrule[empty]{}
   {
     \evalexprlist{\env, \emptylist} \evalarrow \Normal((\emptylist, \emptygraph), \env)
   }
 \and
-  \inferrule[eval\_expr\_list\_nonempty]{
-    \texttt{le} \eqname [\ve] + \vle'\\
-    \evalexpr{\env, \ve} \evalarrow \Normal((\vvone, \vgone), \envp) \OrAbnormal\\
-    \evalexprlist{\envp, \vle'} \evalarrow \Normal((\vvs, \vgtwo), \newenv) \OrAbnormal\\
+  \inferrule[nonempty]{
+    \texttt{le} \eqname [\ve] + \vle1\\
+    \evalexpr{\env, \ve} \evalarrow \Normal((\vvone, \vgone), \envone) \OrAbnormal\\
+    \evalexprlist{\envone, \vle1} \evalarrow \Normal((\vvs, \vgtwo), \newenv) \OrAbnormal\\
     \vg = \vgone \parallel \vgtwo \\
     \vv = [\vvone] + \vvs
   }
@@ -2097,8 +2395,10 @@ \section{SemanticsRule.EExprList \label{sec:SemanticsRule.EExprList}}
     \evalexprlist{\env, \vle} \evalarrow \Normal((\vv, \vg), \newenv)
   }
 \end{mathpar}
+\end{emptyformal}
 
 \section{SemanticsRule.EExprListM \label{sec:SemanticsRule.EExprListM}}
+\subsection{Prose}
 The relation
 \[
   \evalexprlistm{\overname{\envs}{\env} \aslsep \overname{\expr^*}{\vle}} \;\aslrel\;
@@ -2108,32 +2408,40 @@ \section{SemanticsRule.EExprListM \label{sec:SemanticsRule.EExprListM}}
 evaluates a list of expressions $\vle$ in left-to-right in the initial environment $\env$
 and returns the list of values associated with graphs $\vms$ and the new environment $\newenv$.
 If the evaluation of any expression terminates abnormally then the abnormal configuration is returned.
-(Recall that $+$ stands for list concatenation):
+
+\begin{emptyformal}
+\subsection{Formally}
+Recall that $+$ stands for list concatenation.
 \begin{mathpar}
-  \inferrule[eval\_expr\_list\_m\_empty]{}
+  \inferrule[empty]{}
   {
     \evalexprlistm{\env, \emptylist} \evalarrow \Normal((\emptylist, \emptygraph), \env)
   }
 \and
-  \inferrule[eval\_expr\_list\_m\_nonempty]{
-    \vle \eqname [\ve] + \vle'\\
-    \vms \eqname [\vm] + \vms'\\
-    \evalexpr{\env, \ve} \evalarrow \Normal(\vm, \envp) \OrAbnormal\\
-    \evalexprlistm{\envp, \vle'} \evalarrow \Normal(\vms', \newenv) \OrAbnormal\\
+  \inferrule[nonempty]{
+    \vle \eqname [\ve] + \vle1\\
+    \vms \eqname [\vmone] + \vmsone\\
+    \evalexpr{\env, \ve} \evalarrow \Normal(\vmtwo, \envone) \OrAbnormal\\
+    \evalexprlistm{\envone, \vle1} \evalarrow \Normal(\vmstwo, \newenv) \OrAbnormal
   }
   {
-    \evalexprlistm{\env, \vle} \evalarrow \Normal(\vms, \newenv)
+    \evalexprlistm{\env, \vle} \evalarrow \Normal([\vmtwo]+\vmstwo, \newenv)
   }
 \end{mathpar}
+\end{emptyformal}
 
 \section{SemanticsRule.ESideEffectFreeExpr \label{sec:SemanticsRule.ESideEffectFreeExpr}}
+\subsection{Prose}
 The relation
 \[
   \evalexprsef{\overname{\envs}{\env} \aslsep \overname{\expr}{\ve}} \;\aslrel\;
   \Normal(\overname{\vals}{\vv}\aslsep\overname{\XGraphs}{\vg}) \cup
   \overname{\TError}{\ErrorConfig}
 \]
-specializes the expression evaluation relation for side-effect-free expressions:
+specializes the expression evaluation relation for side-effect-free expressions.
+
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
   \inferrule{
     \evalexpr{\env, \ve} \evalarrow \Normal((\vv,\vg), \env) \terminateas \ErrorConfig
@@ -2144,22 +2452,23 @@ \section{SemanticsRule.ESideEffectFreeExpr \label{sec:SemanticsRule.ESideEffectF
 \end{mathpar}
 Notice that the output configuration does not contain an environment,
 since side-effect-free expressions do not modify the environment.
+\end{emptyformal}
 
 \section{SemanticsRule.Lit \label{sec:SemanticsRule.Lit}}
-
-  \subsection{Prose}
-  Evaluation of a literal expression of a value $\vv$
+\subsection{Prose}
+  Evaluation of a literal expression of a value $\vv$, that is $\texttt{E\_Literal}(\vv)$,
   in environment \env\ is the configuration
-  \texttt{\Normal(res,env,g)} and all of the following apply:
+  \texttt{\Normal((\vres,\vg),\newenv)} and all of the following apply:
   \begin{itemize}
   \item $\vres$ is the native value corresponding to $\vv$;
-  \item $\vg$ is the empty graph, as literal do not yield any Read and Write Effects.
+  \item $\vg$ is the empty graph, as literal do not yield any Read and Write Effects;
+  \item $\newenv$ is $\env$.
   \end{itemize}
 
   \subsection{Example}
   In the specification:
     \VerbatimInput{../tests/ASLSemanticsReference.t/SemanticsRule.Lit.asl}
-  the expression \texttt{3} evaluates to the value \texttt{3}.
+  the expression \texttt{3} evaluates to the native value $\nvint(3)$.
 
   \subsection{Code}
   \VerbatimInput[firstline=\LitBegin, lastline=\LitEnd]{../Interpreter.ml}
@@ -2167,23 +2476,23 @@ \section{SemanticsRule.Lit \label{sec:SemanticsRule.Lit}}
 \begin{formal}
   \subsection{Formally}
 \begin{mathpar}
-  \inferrule{\vres = \nvliteral{\vv} \\ \vg = \emptygraph}
-  { \evalexpr{\env, \texttt{E\_Literal}(\vv)} \evalarrow \Normal(\vres, \env, \vg) }
+  \inferrule{\vres = \nvliteral{\vv} \\
+  \vg = \emptygraph \\
+  \newenv \eqname \env}
+  { \evalexpr{\env, \texttt{E\_Literal}(\vv)} \evalarrow \Normal((\vres,\vg), \env) }
 \end{mathpar}
 
 \end{formal}
 
 \isempty{\subsection{Comments}}
 
-
 \section{SemanticsRule.ELocalVar \label{sec:SemanticsRule.ELocalVar}}
-
   \subsection{Prose}
   Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  $\Normal((\vv, \vg), \newenv)$ and all of the following apply:
   \begin{itemize}
-    \item $\ve$ denotes a variable $\vx$ which is bound locally in $\env$;
-    \item $\vres$ is a value $\vv$;
+    \item $\ve$ denotes a variable $\vx$, that is $\evar(\vx)$,
+    which is bound locally in $\env$;
     \item $\vv$ is the value of $\vx$ in $\env$;
     \item $\newenv$ is $\env$.
     \item $\vg$ is the graph containing a single Read Effect for $\vx$.
@@ -2200,11 +2509,14 @@ \section{SemanticsRule.ELocalVar \label{sec:SemanticsRule.ELocalVar}}
 \begin{formal}
   \subsection{Formally}
   \begin{mathpar}
-  \inferrule{\env \eqname (\tenv, \denv)\\
+  \inferrule{
+    \env \eqname (\tenv, \denv)\\
     \vx \in \dom(L^\denv)\\
     \vv = L^\denv(\vx) \\
-    \vg = \ReadEffect(\vx)}
-  {\evalexpr{\env, \evar(\vx)} \evalarrow \Normal((\vv, \vg), \env)}
+    \vg = \ReadEffect(\vx)\\
+    \newenv \eqname \env
+  }
+  {\evalexpr{\env, \evar(\vx)} \evalarrow \Normal((\vv, \vg), \newenv)}
   \end{mathpar}
 \end{formal}
 
@@ -2214,15 +2526,14 @@ \section{SemanticsRule.ELocalVar \label{sec:SemanticsRule.ELocalVar}}
   This is enforced by TypingRule.LDVar and TypingRule.DeclareOneFunc.
 
 \section{SemanticsRule.EGlobalVar \label{sec:SemanticsRule.EGlobalVar}}
-
   \subsection{Prose}
-  Let $\ve$ be an expression denoting a variable \vx.
-  Evaluation of $\ve$ under environment $\env$ terminates normally with
-  \texttt{((v,g),env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is
+  $\Normal((\vv, \vg), \newenv)$ and all of the following apply:
   \begin{itemize}
-  \item \texttt{x} which is bound globally in $\env$;
-  \item $\vv$ is the native value of \texttt{x} in $\env$;
-  \item $\vg$ is the graph containing a single Read Effect for \vx.
+    \item $\ve$ denotes a variable $\vx$, that is $\evar(\vx)$, which is bound globally in $\env$;
+    \item $\vv$ is the value of $\vx$ in $\env$;
+    \item $\newenv$ is $\env$.
+    \item $\vg$ is the graph containing a single Read Effect for $\vx$.
   \end{itemize}
 
   \subsection{Example: SemanticsRuleEGlobalVar.asl}
@@ -2241,22 +2552,24 @@ \section{SemanticsRule.EGlobalVar \label{sec:SemanticsRule.EGlobalVar}}
     \env \eqname (\tenv, \denv)\\
     \vx \in \dom(G^\denv)\\
     \vv = G^\denv(\vx) \\
-    \vg = \ReadEffect(\vx)}
-  {\evalexpr{\denv, \evar(\vx)} \evalarrow \Normal((\vv, \vg), \env)}
+    \vg = \ReadEffect(\vx)\\
+    \newenv \eqname \env
+  }
+  {\evalexpr{\denv, \evar(\vx)} \evalarrow \Normal((\vv, \vg), \newenv)}
   \end{mathpar}
 \end{formal}
 
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.BinopAnd \label{sec:SemanticsRule.BinopAnd}}
-
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is the configuration $C$,
+  and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a conjunction over two expressions \texttt{e1} and \texttt{e2};
-  \item \texttt{(res,new\_env)} is the result of the evaluation of \texttt{if
-e1 then e2 else false} (see Section~\ref{sec:SemanticsRule.ECond}).
+  \item $\ve$ denotes a conjunction over two expressions $\veone$ and $\vetwo$,
+  that is $\texttt{E\_Binop}(\BAND, \veone, \vetwo)$;
+  \item $C$ is the result of the evaluation of the expression
+  \texttt{if e1 then e2 else false} (see \secref{SemanticsRule.ECond}).
   \end{itemize}
   \subsection{Example: SemanticsRule.EBinopAndFalse.asl}
 
@@ -2270,25 +2583,29 @@ \section{SemanticsRule.BinopAnd \label{sec:SemanticsRule.BinopAnd}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexpr{\env, \texttt{E\_Cond}(\texttt{e1}, \texttt{e2}, \efalse)} \evalarrow C
+    \evalexpr{\env, \texttt{E\_Cond}(\veone, \vetwo, \efalse)} \evalarrow C
   }
   {
-  \evalexpr{\env, \texttt{E\_Binop}(\BAND, \texttt{e1}, \texttt{e2})} \evalarrow C
+  \evalexpr{\env, \texttt{E\_Binop}(\BAND, \veone, \vetwo)} \evalarrow C
   }
 \end{mathpar}
 \end{emptyformal}
 
   \subsection{Comments}
+  The evaluation via the rule above ensures that $\veone$ is evaluated first and only if
+  it evalutes to \True, is $\vetwo$ evaluated.
+
   This is related to \identr{BKNT}, \identr{XKGC} and \identi{QRXP}.
 
 \section{SemanticsRule.BinopOr \label{sec:SemanticsRule.BinopOr}}
   \subsection{Prose}
   Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  the configuration $C$ and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a disjunction over two expressions \texttt{e1} and \texttt{e2};
-  \item \texttt{(res,new\_env)} is the result of the evaluation of \texttt{if
-e1 then true else e2} (see Section~\ref{sec:SemanticsRule.ECond}).
+  \item $\ve$ denotes a disjunction over two expressions $\veone$ and $\vetwo$,
+  that is $\texttt{E\_Binop}(\BOR, \veone, \vetwo)$;
+  \item $C$ is the result of the evaluation of
+  \texttt{if e1 then true else e2} (see \secref{SemanticsRule.ECond}).
   \end{itemize}
 
   \subsection{Example: SemanticsRule.EBinopOrTrue.asl}
@@ -2301,23 +2618,26 @@ \section{SemanticsRule.BinopOr \label{sec:SemanticsRule.BinopOr}}
 \begin{emptyformal}
   \begin{mathpar}
     \inferrule{
-      \evalexpr{\env, \texttt{E\_Cond}(\texttt{e1}, \etrue, \texttt{e2})} \evalarrow C
+      \evalexpr{\env, \texttt{E\_Cond}(\veone, \etrue, \texttt{e2})} \evalarrow C
     }
     {
-    \evalexpr{\env, \texttt{E\_Binop}(\BOR, \texttt{e1}, \texttt{e2})} \evalarrow C
+    \evalexpr{\env, \texttt{E\_Binop}(\BOR, \veone, \texttt{e2})} \evalarrow C
     }
   \end{mathpar}
+  The evaluation via the rule above ensures that $\veone$ is evaluated first and only if
+  it evalutes to \True, is $\vetwo$ evaluated.
 \end{emptyformal}
 
   \subsection{Comments}
   This is related to \identr{BKNT}, \identr{XKGC} and \identi{QRXP}.
 
 \section{SemanticsRule.BinopImpl \label{sec:SemanticsRule.BinopImpl}}
-
   \subsection{Prose}
-  All of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is
+  the configuration $C$ and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes an implication over two expressions \texttt{e1} and \texttt{e2};
+  \item $\ve$ denotes an implication over two expressions $\veone$ and $\vetwo$,
+  that is $\texttt{E\_Binop}(\IMPL, \veone, \vetwo)$;
   \item $\ve$ is evaluated as \texttt{if e1 then e2 else true}.
   \end{itemize}
 
@@ -2330,12 +2650,14 @@ \section{SemanticsRule.BinopImpl \label{sec:SemanticsRule.BinopImpl}}
 \begin{emptyformal}
   \begin{mathpar}
     \inferrule{
-      \evalexpr{\env, \texttt{E\_Cond}(\texttt{e1}, \texttt{e2}, \etrue)} \evalarrow C
+      \evalexpr{\env, \texttt{E\_Cond}(\veone, \vetwo, \etrue)} \evalarrow C
     }
     {
-    \evalexpr{\env, \texttt{E\_Binop}(\IMPL, \texttt{e1}, \texttt{e2})} \evalarrow C
+    \evalexpr{\env, \texttt{E\_Binop}(\IMPL, \veone, \vetwo)} \evalarrow C
     }
   \end{mathpar}
+  The evaluation via the rule above ensures that $\veone$ is evaluated first and only if
+  it evalutes to \True, is $\vetwo$ evaluated.
 \end{emptyformal}
 
 \subsection{Comments}
@@ -2344,16 +2666,22 @@ \subsection{Comments}
 \section{SemanticsRule.Binop \label{sec:SemanticsRule.Binop}}
 
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either $\Normal((\vv, \vg), \newenv)$,
+  or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-    \item $\ve$ denotes a Binary Operator \texttt{op} over two expressions \texttt{e1} and \texttt{e2};
-    \item The evaluation of the expression \texttt{e1} under $\env$ is \texttt{v1};
-    \item $\envp$ is the result of modifying $\env$ after evaluation of the expression \texttt{e1} under $\env$;
-    \item The evaluation of the expression \texttt{e2} under $\env$ is \texttt{v2};
-    \item $\newenv$ is the result of modifying $\envp$ after evaluation of the expression \texttt{e2} under $\envp$;
-    \item $\vv$ is the result of applying the Binary Operator \texttt{op} to \texttt{v1} and \texttt{v2};
-    \item $\vres$ is $\vv$;
-    \item $\newenv$ is $\env$.
+    \item $\ve$ denotes a Binary Operator $\op$ over two expressions $\veone$ and $\vetwo$,
+    that is $\texttt{E\_Binop}(\op, \veone, \vetwo)$;
+    \item the operator is not one of $\BAND$, $\BOR$, or $\IMPL$, which are handled by the
+    rule presented previoiusly;
+    \item the evaluation of the expression $\veone$ under $\env$ is the configuration $\Normal(\vmone, \envone)$,
+    \ProseOrAbnormal;
+    \item the evaluation of the expression $\vetwo$ under $\envone$ is the configuration $\Normal(\vmtwo, \newenv)$,
+    \ProseOrAbnormal;
+    \item $\vmone$ consists of the value $\vvone$ and the execution graph $\vgone$;
+    \item $\vmtwo$ consists of the value $\vvtwo$ and the execution graph $\vgtwo$;
+    \item applying the Binary Operator $\op$ to $\vvone$ and $\vvtwo$ results in either $\vv$,
+    or an error, which short-circuits the entire evaluation;
+    \item $\vg$ is the parallel composition of $\vgone$ and $\vgtwo$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.EBinopPlusAssert.asl}
@@ -2377,9 +2705,9 @@ \section{SemanticsRule.Binop \label{sec:SemanticsRule.Binop}}
 \begin{formal}
   \subsection{Formally}
   \begin{mathpar}
-    \inferrule{
-      \evalexpr{ \env, \veone} \evalarrow \Normal(\vmone, \envp) \OrAbnormal \\\\
-      \evalexpr{ \envp, \vetwo } \evalarrow \Normal(\vmtwo, \newenv) \OrAbnormal \\\\
+    \inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\
+      \evalexpr{ \env, \veone} \evalarrow \Normal(\vmone, \envone) \OrAbnormal \\\\
+      \evalexpr{ \envone, \vetwo } \evalarrow \Normal(\vmtwo, \newenv) \OrAbnormal \\\\
       \vmone \eqname (\vvone, \vgone) \\
       \vmtwo \eqname (\vvtwo, \vgtwo) \\
       \binop(\op, \vvone, \vvtwo) \evalarrow \vv \terminateas \ErrorConfig\\\\
@@ -2390,6 +2718,8 @@ \section{SemanticsRule.Binop \label{sec:SemanticsRule.Binop}}
       \Normal((\vv, \vg), \newenv)
     }
   \end{mathpar}
+  The rule above applies to many binary operators, including $\EQOP$ (which is used for \texttt{<->}
+  as well as \texttt{==}).
 \end{formal}
 
 \subsection{Comments}
@@ -2404,11 +2734,13 @@ \subsection{Comments}
 
 \section{SemanticsRule.Unop \label{sec:SemanticsRule.Unop}}
   \subsection{Prose}
-  All of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either $\Normal((\vv, \vg), \newenv)$,
+  or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a Unary Operator \texttt{op} over an expression \texttt{e'} in an environment $\env$;
-  \item The evaluation of the expression \texttt{e'} under $\env$ is \texttt{v',new\_env};
-  \item \texttt{v, new\_env} is the result of applying the Unary Operator \texttt{op} to \texttt{v'}.
+  \item $\ve$ denotes a Unary Operator $\op$ over an expression $\veone$, that is\\ $\texttt{E\_Unop}(\op, \veone)$;
+  \item the evaluation of the expression $\veone$ under $\env$ is either \\ $\Normal((\vvone, \vg), \newenv)$,
+  or an abnormal configuration, which circuits the entire evaluation;
+  \item applying the Unary Operator $\op$ to $\vvone$ is $\vv$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.EUnopAssert.asl}
@@ -2422,11 +2754,11 @@ \section{SemanticsRule.Unop \label{sec:SemanticsRule.Unop}}
 \begin{emptyformal}
 \begin{mathpar}
   \inferrule{
-    \evalexpr{ \env, \vep} \evalarrow \Normal((\vvp,\vg), \newenv)\\
-    \unop(\op, \vvp) \evalarrow \vv
+    \evalexpr{ \env, \veone} \evalarrow \Normal((\vvone,\vg), \newenv) \OrAbnormal\\
+    \unop(\op, \vvone) \evalarrow \vv
   }
   {
-    \evalexpr{ \env, \texttt{E\_Unop}(\op, \vep) } \evalarrow
+    \evalexpr{ \env, \texttt{E\_Unop}(\op, \veone) } \evalarrow
     \Normal((\vv, \vg), \newenv)
   }
   \end{mathpar}
@@ -2437,11 +2769,30 @@ \section{SemanticsRule.Unop \label{sec:SemanticsRule.Unop}}
 \section{SemanticsRule.ECond \label{sec:SemanticsRule.ECond}}
 
   \subsection{Prose}
-  All of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either $\Normal((\vv, \vg), \newenv)$,
+  or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-    \item $\ve$ denotes a conditional expression \texttt{e\_cond} with two options \texttt{e1} and \texttt{e2};
-    \item The evaluation of the conditional expression \texttt{e\_cond} under $\env$ is \texttt{m\_cond};
-    \item The evaluation of \texttt{e1} or \texttt{e2}, depending on \texttt{m\_cond}, is $\vv$.
+    \item $\ve$ denotes a conditional expression $\econd$ with two options $\veone$ and $\vetwo$,
+    that is $\texttt{E\_Cond}(\texttt{e\_cond}, \veone, \vetwo)$;
+    \item the evaluation of the conditional expression $\econd$ under $\env$ is either
+    $\Normal(\mcond, \envone)$, \ProseOrAbnormal;
+    \item One of the following applies:
+    \begin{itemize}
+      \item all of the following apply:
+      \begin{itemize}
+      \item $\mcond$ is the native Boolean \True\ and execution graph $\vgone$;
+      \item the evaluation of $\veone$ under $\envone$ is either $\Normal((\vvtwo, \vgtwo), \newenv)$,
+      \ProseOrAbnormal;
+      \end{itemize}
+
+      \item all of the following apply:
+      \begin{itemize}
+      \item $\mcond$ is the native Boolean \False\ and execution graph $\vgone$;
+      \item the evaluation of $\vetwo$ under $\envone$ is either $\Normal((\vvtwo, \vgtwo), \newenv)$,
+      \ProseOrAbnormal;
+      \end{itemize}
+    \end{itemize}
+      \item $\vg$ is the parallel composition of $\vgone$ and $\vgtwo$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.ECondFalse.asl}
@@ -2461,10 +2812,10 @@ \section{SemanticsRule.ECond \label{sec:SemanticsRule.ECond}}
 
 \begin{emptyformal}
 \begin{mathpar}
-  \inferrule[(Condition True)]{
-    \evalexpr{\env, \texttt{e\_cond}} \evalarrow \Normal(\mcond, \envp) \OrAbnormal\\
+  \inferrule[True]{
+    \evalexpr{\env, \texttt{e\_cond}} \evalarrow \Normal(\mcond, \envone) \OrAbnormal\\
     \mcond \eqname (\nvbool(\True), \vgone)\\
-    \evalexpr{\envp, \veone} \evalarrow \Normal((\vv, \vgtwo), \newenv)  \OrAbnormal\\
+    \evalexpr{\envone, \veone} \evalarrow \Normal((\vv, \vgtwo), \newenv)  \OrAbnormal\\
     \vg = \ordered{\vgone}{\aslctrl}{\vgtwo}
   }
   {
@@ -2472,10 +2823,10 @@ \section{SemanticsRule.ECond \label{sec:SemanticsRule.ECond}}
     \Normal((\vv, \vg), \newenv)
   }
 \and
-\inferrule[(Condition False)]{
-  \evalexpr{\env, \texttt{e\_cond}} \evalarrow \Normal(\mcond, \envp) \OrAbnormal\\
+\inferrule[False]{
+  \evalexpr{\env, \texttt{e\_cond}} \evalarrow \Normal(\mcond, \envone) \OrAbnormal\\
   \mcond \eqname (\nvbool(\False), \vgone)\\
-  \evalexpr{\envp, \vetwo} \evalarrow \Normal((\vv, \vgtwo), \newenv)  \OrAbnormal\\
+  \evalexpr{\envone, \vetwo} \evalarrow \Normal((\vv, \vgtwo), \newenv)  \OrAbnormal\\
   \vg = \ordered{\vgone}{\aslctrl}{\vgtwo}
 }
 {
@@ -2490,18 +2841,29 @@ \section{SemanticsRule.ECond \label{sec:SemanticsRule.ECond}}
 
 \section{SemanticsRule.ESlice \label{sec:SemanticsRule.ESlice}}
   \subsection{Prose}
-  All of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either $\Normal((\vv, \vg), \newenv)$,
+  or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-    \item $\ve$ denotes an expression \texttt{e\_bv} sliced as per \texttt{slices};
-    \item The evaluation of \texttt{e\_bv} under $\env$ is \texttt{v\_bv};
-    \item The evaluation of \texttt{slices} under $\env$ is \texttt{positions};
-    \item $\vv$ is the value read in \texttt{v\_bv} from \texttt{positions}.
+    \item $\ve$ denotes an expression $\ebv$ sliced as per $\slices$,
+    that is $\texttt{E\_Slice}(\ebv, \slices)$;
+    \item the evaluation of $\ebv$ under $\env$ is either $\Normal(\mbv, \envone)$,
+    \ProseOrAbnormal;
+    \item the evaluation of $\slices$ under $\env$ is either $\Normal(\mpositions, \envone)$,
+    \ProseOrAbnormal;
+    \item $\mpositions$ consists of $\positions$ --- all the indices that need to be added to the
+    resulting bitvector --- and the execution graph $\vgone$;
+    \item reading from $\vbv$ as a bitvector at the indices indicated by $\positions$
+    (see \secref{SemanticsRule.ReadFromBitvector}) either results in the bitvector $\vv$,
+    which concatenates all of the values from the indicates indices,
+    \ProseOrError;
+    \item $\newenv$ is $\envone$;
+    \item $\vg$ is the parallel composition of $\vgone$ and $\vgtwo$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.ESlice.asl}
     In the specification:
     \VerbatimInput{../tests/ASLSemanticsReference.t/SemanticsRule.ESlice.asl}
-    the expression \texttt{'11110000'[5:2]} evaluates to the value \texttt{'1100'}.
+    the expression \texttt{'11110000'[6:3]} evaluates to the value \texttt{'1110'}.
 
   \subsection{Code}
   \VerbatimInput[firstline=\ESliceBegin, lastline=\ESliceEnd]{../Interpreter.ml}
@@ -2510,12 +2872,12 @@ \section{SemanticsRule.ESlice \label{sec:SemanticsRule.ESlice}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexpr{\env, \ebv} \evalarrow \Normal(\mbv, \envone)  \OrAbnormal\\
+    \evalexpr{\env, \ebv} \evalarrow \Normal(\mbv, \envone)  \OrAbnormal\\\\
     \mbv \eqname (\vbv,\vgone) \\
-    \evalslices{\envone, \slices} \evalarrow \Normal(\mpositions, \envp)  \OrAbnormal \\
+    \evalslices{\envone, \slices} \evalarrow \Normal(\mpositions, \envone)  \OrAbnormal \\
     \mpositions \eqname (\positions, \vgtwo) \\
     \readfrombitvector(\vbv, \positions) \evalarrow \vv \terminateas \ErrorConfig\\
-    \newenv = \envp \\
+    \newenv = \envone \\
     \vg = \vgone \parallel \vgtwo
   }
   {
@@ -2527,14 +2889,30 @@ \section{SemanticsRule.ESlice \label{sec:SemanticsRule.ESlice}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.ECall \label{sec:SemanticsRule.ECall}}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either $\Normal((\vv, \vg), \newenv)$,
+  or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-    \item $\ve$ denotes a subprogram call \texttt{(name, params, actual\_args)};
-    \item The evaluation of that subprogram call under $\env$ is \texttt{ms};
-    \item $\vres$ is a value $\vv$;
-    \item $\vv$ is the value read from \texttt{ms};
-    \item $\newenv$ is $\env$.
+    \item $\ve$ denotes a subprogram call $(\name, \actualargs, \params)$,
+    that is \\ $\texttt{E\_Call}(\name, \actualargs, \params)$;
+    \item the evaluation of that subprogram call under $\env$ is either
+    $\Normal(\vms, \newenv)$, or an abnormal configuration,
+    which short-circuits the entire evaluation;
+    \item one of the following apply:
+    \begin{itemize}
+      \item all of the following apply (\textsc{single\_returned\_value}):
+      \begin{itemize}
+        \item $\vms$ consists of a single returned value $(\vv,\vg)$,
+        which go into the output configuration $\Normal((\vv, \vg), \newenv)$.
+      \end{itemize}
+
+      \item all of the following apply (\textsc{multipe\_returned\_values}):
+      \begin{itemize}
+        \item $\vms$ consists of a list of returned value $(\vv_i,\vg_i)$, for $i=1..k$;
+        \item $\vg$ is the parallel composition of $\vg_i$, for $i=1..k$;
+        \item $\vv$ is the native value vector of values $\vv_i$, for $i=1..k$;
+        \item the resulting configuration is $\Normal((\vv, \vg), \newenv)$.
+      \end{itemize}
+    \end{itemize}
   \end{itemize}
 
   \subsection{Example: SemanticsRule.ECall.asl}
@@ -2549,16 +2927,16 @@ \section{SemanticsRule.ECall \label{sec:SemanticsRule.ECall}}
 \begin{emptyformal}
   \subsection{Formally}
 \begin{mathpar}
-  \inferrule[(Single returned value)]{
-    \evalcall{\env, \name, \actualargs, \params} \evalarrow \Normal(\vms, \newenv)  \OrAbnormal\\
+  \inferrule[single\_returned\_value]{
+    \evalcall{\env, \name, \actualargs, \params} \evalarrow \Normal(\vms, \newenv) \OrAbnormal\\
     \vms \eqname [(\vv, \vg)]
   }
   {
     \evalexpr{\env, \texttt{E\_Call}(\name, \actualargs, \params)} \evalarrow \Normal((\vv, \vg), \newenv)
   }
 \and
-\inferrule[(Multiple returned values)]{
-  \evalcall{\env, \name, \actualargs, \params} \evalarrow \Normal(\vms, \newenv)  \OrAbnormal\\
+\inferrule[multiple\_returned\_values]{
+  \evalcall{\env, \name, \actualargs, \params} \evalarrow \Normal(\vms, \newenv) \OrAbnormal\\
   \vms \eqname [i=1..k: (\vv_i, \vg_i)]\\
   \vg = \vg_1 \parallel \ldots \parallel \vg_k \\
   \vv = \nvvector{\vv_{1..k}}
@@ -2574,30 +2952,26 @@ \section{SemanticsRule.ECall \label{sec:SemanticsRule.ECall}}
 \section{SemanticsRule.EGetArray \label{sec:SemanticsRule.EGetArray}}
 
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  such that all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either \\
+  $\Normal((\vv, \vg), \newenv)$, or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes an array \texttt{e\_array} and an index \texttt{e\_index};
-  \item The evaluation of \texttt{e\_array} under $\env$ is \texttt{v\_array};
-  \item The evaluation of \texttt{e\_index} under $\env$ is \texttt{v\_index};
-  \item One of the following applies:
-        \begin{itemize}
-        \item All of the following apply:
-          \begin{itemize}
-          \item the result of evaluation of $\ve$ under $\env$ is \texttt{(res, env)};
-          \item $\vres$ is a value $\vv$;
-          \item $\vv$ is the value found at the index \texttt{v\_index} of \texttt{v\_array};
-          \item $\newenv$ is $\env$;
-          \end{itemize}
-
-        \item $\vres$ is a typing error.
-        \end{itemize}
+  \item $\ve$ denotes an array $\earray$ and an index $\eindex$,
+  that is $\texttt{E\_GetArray}(\earray, \eindex)$;
+  \item the evaluation of $\earray$ under $\env$ is either $\Normal(\marray, \envone)$,
+  \ProseOrAbnormal;
+  \item the evaluation of $\eindex$ under $\env$ is either  $\Normal(\mindex, \newenv)$,
+  \ProseOrAbnormal;
+  \item $\marray$ consists of the native vector $\varray$ and execution graph $\vgone$;
+  \item $\mindex$ consists of the native integer $\vindex$ and execution graph $\vgtwo$;
+  \item $\vindex$ is the native integer for $\vi$;
+  \item evaluating the value at index $\vi$ of $\varray$ is $\vv$;
+  \item $\vg$ is the parallel composition of $\vgone$ and $\vgtwo$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.EGetArray.asl}
     In the specification:
     \VerbatimInput{../tests/ASLSemanticsReference.t/SemanticsRule.EGetArray.asl}
-    the expression \texttt{my\_array[2]} evaluates to the value \texttt{42} since the element
+    the expression \texttt{my\_array[2]} appearing in the assertion evaluates to the value \texttt{42} since the element
     indexed by \texttt{2} in \texttt{my\_array} is \texttt{42}.
 
   \subsection{Example: SemanticsRule.EGetArrayTooSmall.asl}
@@ -2632,22 +3006,25 @@ \section{SemanticsRule.EGetArray \label{sec:SemanticsRule.EGetArray}}
 \section{SemanticsRule.ERecord \label{sec:SemanticsRule.ERecord}}
 
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either \\
+  $\Normal((\vv, \vg), \newenv)$, or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a record value \texttt{names} and associated expressions
-    \texttt{fields};
-  \item \texttt{fields} evaluates in $\env$ to \texttt{v\_fields};
-  \item $\vres$ is a value $\vv$;
-  \item $\vv$ is the record built by associating the names \texttt{names} to \texttt{v\_fields}.
-  \item $\newenv$ is $\env$.
+  \item $\ve$ denotes a record value $\names$ and associated expressions
+    $\efields$, that is $\texttt{E\_Record}(\names, \efields)$;
+  \item the names of of the fields are $\id_{1..k}$;
+  \item the expressions associated with the fields are $\ve_{1..k}$;
+  \item evaluating the expressions of $\fields$ in order either
+  results in \\
+  $\Normal((\vvfields,\vg), \newenv)$, \ProseOrAbnormal;
+  \item $\vvfields$ is a list of native values $\vv_{1..k}$;
+  \item $\vv$ is the native record that maps $\id_i$ to $\vv_i$, for $i=1..k$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.ERecord.asl}
     In the specification:
     \VerbatimInput{../tests/ASLSemanticsReference.t/SemanticsRule.ERecord.asl}
-    the expression \texttt{MyRecordType { a=3, b=42 }} evaluates to the value \texttt{{a:
-3, b: 42}}.
+    the expression \texttt{MyRecordType \{ a=3, b=42 \}} evaluates to the value
+    \texttt{\{a: 3, b: 42\}}.
 
   \subsection{Code}
   \VerbatimInput[firstline=\ERecordBegin, lastline=\ERecordEnd]{../Interpreter.ml}
@@ -2657,12 +3034,11 @@ \section{SemanticsRule.ERecord \label{sec:SemanticsRule.ERecord}}
 \begin{mathpar}
   \inferrule{
     \efields \eqname [i=1..k: (\id_i, \ve_i)]\\
-    \names = [i=1..k: \id_i] \\
-    \fields = [i=1..k: \ve_i] \\
-    \evalexprlist{\env, \fields} \evalarrow \Normal((\vvfields,\vg), \envp)  \OrAbnormal\\
-    \vvfields = (i=1..k: \vv_i)\\
-    \vv = \nvrecord{\{i=1..k: \id_i\mapsto \vv_i\}}\\
-    \newenv = \envp
+    \names = \id_{1..k} \\
+    \fields = \ve_{1..k} \\
+    \evalexprlist{\env, \fields} \evalarrow \Normal((\vvfields,\vg), \newenv)  \OrAbnormal\\
+    \vvfields = \vv_{1..k}\\
+    \vv = \nvrecord{\{i=1..k: \id_i\mapsto \vv_i\}}
   }
   {
     \evalexpr{\env, \texttt{E\_Record}(\Ignore, \efields)} \evalarrow \Normal((\vv, \vg), \newenv)
@@ -2673,16 +3049,15 @@ \section{SemanticsRule.ERecord \label{sec:SemanticsRule.ERecord}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.EGetField \label{sec:SemanticsRule.EGetField}}
-
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either \\
+  $\Normal((\vv, \vg), \newenv)$, or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a field name \texttt{field\_name} in a record value \texttt{e\_vec};
-  \item the evaluation of \texttt{e\_vec} in $\env$ is \texttt{v\_vec};
-  \item $\vres$ is a value $\vv$;
-  \item $\vv$ is the value mapped by \texttt{field\_name} in \texttt{v\_vec};
-  \item $\newenv$ is $\env$.
+  \item $\ve$ denotes a field name $\fieldname$ in a record value $\erecord$,
+  that is $\texttt{E\_GetField}(\erecord, \fieldname)$;
+  \item the evaluation of $\erecord$ in $\env$ is either $\Normal((\vrecord, \vg), \newenv)$,
+  \ProseOrAbnormal;
+  \item $\vv$ is the value mapped by $\fieldname$ in the native record $\vrecord$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.ERecord.asl}
@@ -2697,9 +3072,8 @@ \section{SemanticsRule.EGetField \label{sec:SemanticsRule.EGetField}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexpr{\env, \erecord} \evalarrow \Normal((\vrecord, \vg), \envp)  \OrAbnormal\\
-    \getfield(\fieldname, \vrecord) = \vv\\
-    \newenv = \envp
+    \evalexpr{\env, \erecord} \evalarrow \Normal((\vrecord, \vg), \newenv)  \OrAbnormal\\
+    \getfield(\fieldname, \vrecord) \evalarrow \vv
   }
   {
     \evalexpr{\env, \texttt{E\_GetField}(\erecord, \fieldname)} \evalarrow \Normal((\vv, \vg), \newenv)
@@ -2707,20 +3081,17 @@ \section{SemanticsRule.EGetField \label{sec:SemanticsRule.EGetField}}
 \end{mathpar}
 \end{emptyformal}
 
-
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.EConcat \label{sec:SemanticsRule.EConcat}}
-
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either \\
+  $\Normal((\vv, \vg), \newenv)$, or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a list of bitvector expressions \texttt{e\_list};
-  \item the evaluation of \texttt{e\_list} in $\env$ is \texttt{v\_list};
-  \item $\vres$ is a value $\vv$;
-  \item $\vv$ is the concatenation of \texttt{v\_list};
-  \item $\newenv$ is $\env$.
+  \item $\ve$ denotes a list of bitvector expressions $\elist$, that is $\texttt{E\_Concat}(\elist)$;
+  \item the evaluation of $\elist$ in $\env$ is either $\Normal((\vlist, \vg), \newenv)$,
+  \ProseOrAbnormal;
+  \item $\vv$ is the bitvector constructed from the concatenation of $\vlist$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.EConcat}
@@ -2735,9 +3106,8 @@ \section{SemanticsRule.EConcat \label{sec:SemanticsRule.EConcat}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexprlist{\env, \elist} \evalarrow \Normal((\vlist, \vg), \envp)  \OrAbnormal\\
-    \concatbitvectors(\vlist) = \vv\\
-    \newenv = \envp
+    \evalexprlist{\env, \elist} \evalarrow \Normal((\vlist, \vg), \newenv)  \OrAbnormal\\
+    \concatbitvectors(\vlist) \evalarrow \vv
   }
   {
     \evalexpr{\env, \texttt{E\_Concat}(\elist)} \evalarrow \Normal((\vv, \vg), \newenv)
@@ -2749,16 +3119,14 @@ \subsection{Comments}
   This is related to \identr{BRCM}.
 
 \section{SemanticsRule.ETuple \label{sec:SemanticsRule.ETuple}}
-
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is either \\
+  $\Normal((\vv, \vg), \newenv)$, or an abnormal configuration, and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a list of expression \texttt{e\_list};
-  \item the evaluation of \texttt{e\_list} in $\env$ is \texttt{v\_list};
-  \item $\vres$ is a value $\vv$;
-  \item $\vv$ is the tuple built from \texttt{v\_list};
-  \item $\newenv$ is $\env$.
+  \item $\ve$ denotes a tuple over a list of expressions $\elist$, that is $\texttt{E\_Tuple}(\elist)$;
+  \item the evaluation of $\elist$ in $\env$ is either $\Normal((\vlist, \vg), \newenv)$,
+  \ProseOrAbnormal;
+  \item $\vv$ is the native vector constructed from the values in $\vlist$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.ETuple.asl}
@@ -2773,9 +3141,8 @@ \section{SemanticsRule.ETuple \label{sec:SemanticsRule.ETuple}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexprlist{\env, \elist} \evalarrow \Normal((\vlist, \vg), \envp)  \OrAbnormal\\
-    \vv = \nvvector{\vlist}\\
-    \newenv = \envp
+    \evalexprlist{\env, \elist} \evalarrow \Normal((\vlist, \vg), \newenv)  \OrAbnormal\\
+    \vv = \nvvector{\vlist}
   }
   {
     \evalexpr{\env, \texttt{E\_Tuple}(\elist)} \evalarrow \Normal((\vv, \vg), \newenv)
@@ -2786,22 +3153,20 @@ \section{SemanticsRule.ETuple \label{sec:SemanticsRule.ETuple}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.EUnknown \label{sec:SemanticsRule.EUnknown}}
-
   \paragraph{Domain of a Type}
-
   The domain of a type $\vt$ in an environment $\env=(\tenv,\denv)$,
   denoted by $\textsf{dyn-dom}(\tenv, \denv, \vt)$, is defined by the type system~\cite{ASLTypingReference}
   (TypingRule.Domain)
-  as the set of values that $\vt$ may store. The reason that the dynamic environment is
+  as the set of values that $\vt$ may store in $\env$. The reason that the dynamic environment is
   needed to determine the domain is due to subprogram parameters, which constrain integer parameters to
   a singleton value domain.
 
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ terminates normally with
-  \texttt{(v,new\_env,g)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is \\
+  $\Normal((\vv, \vg), \newenv)$ and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes the \texttt{UNKNOWN} expression annotated with type \texttt{t};
-  \item $\vv$ is a value in the domain of \texttt{t};
+  \item $\ve$ denotes the \texttt{UNKNOWN} expression annotated with type $\vt$;
+  \item $\vv$ is a value in the domain of $\vt$ in $\env$;
   \item $\newenv$ is $\env$.
   \item $\vg$ is the empty execution graph.
   \end{itemize}
@@ -2838,16 +3203,17 @@ \subsection{Comments}
   This is related to \identr{WLCH}.
 
 \section{SemanticsRule.EPattern \label{sec:SemanticsRule.EPattern}}
-
-
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is \\
+  $\Normal((\vv, \vg), \newenv)$ and all of the following apply:
   \begin{itemize}
-  \item $\ve$ denotes a pattern \texttt{e,p};
-  \item $\vres$ is a value $\vv$;
-  \item $\vv$ is the boolean determining whether the evaluation of $\ve$ in $\env$ matches $\vp$;
-  \item $\newenv$ is $\env$.
+  \item $\ve$ denotes a pattern $\ve, \vp$, that is $\texttt{E\_Pattern}(\ve, \vp)$;
+  \item evaluating the expression $\ve$ under environment $\env$ either results in \\
+  $\Normal((\vvone, \vgone), \newenv)$, \ProseOrAbnormal;
+  \item evaluating whether the pattern $\vp$ matches the value $\vvone$ under $\env$
+  results in $\Normal(\vv, \vgtwo)$ where is a native Boolean that determines
+  whether the is indeed a match;
+  \item $\vg$ is the ordered composition of $\vgone$ and $\vgtwo$ with the data label.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.EPatternFALSE.asl}
@@ -2867,9 +3233,8 @@ \section{SemanticsRule.EPattern \label{sec:SemanticsRule.EPattern}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexpr{\env, \ve} \evalarrow \Normal((\vvone, \vgone), \envp)  \OrAbnormal\\
+    \evalexpr{\env, \ve} \evalarrow \Normal((\vvone, \vgone), \newenv)  \OrAbnormal\\
     \evalpattern{\env, \vvone, \vp} \evalarrow \Normal(\vv, \vgtwo)\\
-    \newenv = \envp\\
     \vg = \ordered{\vgone}{\asldata}{\vgtwo}
   }
   {
@@ -2881,26 +3246,26 @@ \section{SemanticsRule.EPattern \label{sec:SemanticsRule.EPattern}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.CTC \label{sec:SemanticsRule.CTC}}
-
   \subsection{Prose}
-  Evaluation of the expression $\ve$ under environment $\env$ is
-  \texttt{(res,new\_env)} and all of the following apply:
+  Evaluation of the expression $\ve$ under environment $\env$ is \\
+  $\Normal((\vv, \vg), \newenv)$ and all of the following apply:
   \begin{itemize}
-  \item \texttt{(e,\_t)} denotes an expression $\ve$ and a type \texttt{t};
-  \item $\vv$ is the result of evaluating $\ve$ in $\env$;
-  \item $\newenv$ is $\env$ modified after evaluating $\ve$ in $\env$;
-  \item \texttt{b} is \texttt{true} or \texttt{false} depending on whether $\vv$ is of type \texttt{t} in $\env$;
-  \item One of the following applies:
+  \item $(\ve, \vt)$ denotes an expression $\ve$ and a type $\vt$,
+  that is $\texttt{E\_CTC}(\ve, \vt)$;
+  \item evaluating $\ve$ under $\env$ either results in \Normal((\vv, \vgone), \newenv),
+  \ProseOrAbnormal;
+  \item evaluating whether $\vv$ has type $\vt$ under $\env$ either results in (\vb, \vgtwo)
+  or in an error configuration, which short-circuits the entire evaluation;
+  \item one of the following applies:
         \begin{itemize}
-        \item All of the following apply:
+        \item all of the following apply (\textsc{okay}):
               \begin{itemize}
-              \item \texttt{b} is \texttt{true};
-              \item $\vres$ is $\vv$;
-              \item $\newenv$ is $\newenv$
+              \item $\vb$ is the native Boolean for \True;
+              \item $\vg$ is the ordered composition of $\vgone$ and $\vgtwo$ with the data label.
               \end{itemize}
-        \item All of the following apply:
+        \item all of the following apply (\textsc{error}):
               \begin{itemize}
-              \item \texttt{b} is \texttt{false};
+              \item $\vb$ is the native Boolean for \True;
               \item a type conversion error is returned.
               \end{itemize}
         \end{itemize}
@@ -2919,7 +3284,7 @@ \section{SemanticsRule.CTC \label{sec:SemanticsRule.CTC}}
 \begin{emptyformal}
   \subsection{Formally}
 \begin{mathpar}
-  \inferrule{
+  \inferrule[okay]{
     \evalexpr{\env, \ve} \evalarrow \Normal((\vv, \vgone), \newenv)  \OrAbnormal\\
     \isvaloftype(\env, \vv, \vt) \evalarrow (\vb, \vgtwo) \terminateas \ErrorConfig\\
     \vb \eqname \nvbool(\True)\\
@@ -2929,13 +3294,13 @@ \section{SemanticsRule.CTC \label{sec:SemanticsRule.CTC}}
     \evalexpr{\env, \texttt{E\_CTC}(\ve, \vt)} \evalarrow \Normal((\vv, \vg), \newenv)
   }
 \and
-\inferrule{
+\inferrule[error]{
   \evalexpr{\env, \ve} \evalarrow \Normal((\vv, \Ignore), \Ignore)\\
   \neg\isvaloftype(\env, \vv, \vt) \evalarrow (\vb, \Ignore)\\
   \vb \eqname \nvbool(\False)
 }
 {
-  \evalexpr{\env, \texttt{E\_CTC}(\ve, \vt)} \evalarrow \Error(\texttt{"Type mismatch!"})
+  \evalexpr{\env, \texttt{E\_CTC}(\ve, \vt)} \evalarrow \ErrorVal{CTC\_TypeMismatch}
 }
 \end{mathpar}
 \end{emptyformal}
@@ -2950,12 +3315,16 @@ \chapter{Evaluation of Left-Hand Side Expressions \label{chap:eval_lexpr}}
 The relation
 \[
   \evallexpr{\overname{\envs}{\env} \aslsep \overname{\lexpr}{\vle} \aslsep (\overname{\vals}{\vv} \times \overname{\XGraphs}{\vg})} \;\aslrel\;
-    \Normal(\overname{\XGraphs}{\vgp},\overname{\envs}{\newenv}) \cup
+    \Normal(\overname{\XGraphs}{\newg},\overname{\envs}{\newenv}) \cup
     \overname{\TThrowing}{\ThrowingConfig} \cup \overname{\TError}{\ErrorConfig}
 \]
-evaluates the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is either $\newenv$
-or an error is returned and one of the following applies:
+evaluates the assignment of a value $\vv$
+to the left-hand-side expression $\vle$ under an environment $\env$,
+resulting in either in a configuration $\Normal(\newg, \env)$ or an abnormal configuration.
+
+We first define the helper rule SemanticsRule.LEMultiAssign (\ref{sec:SemanticsRuleLEMultiAssign}).
+
+One of the following applies:
 \begin{itemize}
 \item SemanticsRule.LEDiscard (see Section~\ref{sec:SemanticsRule.LEDiscard});
 \item SemanticsRule.LELocalVar (see Section~\ref{sec:SemanticsRule.LELocalVar});
@@ -2966,45 +3335,59 @@ \chapter{Evaluation of Left-Hand Side Expressions \label{chap:eval_lexpr}}
 \item SemanticsRule.LEDestructuring (see Section~\ref{sec:SemanticsRule.LEDestructuring}).
 \end{itemize}
 
+Some of the rules require viewing left-hand-side expressions as their corresponding right-hand side expressions.
+The correspondence is defined in the ASL Syntax Reference~\cite[Chapter 5]{ASLAbstractSyntaxReference}
+and given by the function $\torexpr : \lexpr \rightarrow \expr$.
+
 \section{SemanticsRule.LEMultiAssign \label{sec:SemanticsRuleLEMultiAssign}}
+\subsection{Prose}
 The helper relation
 \[
-  \evalmultiassignment{\overname{\envs}{\env} \aslsep \overname{\expr^*}{\vlelist} \aslsep \overname{(\vals \times \XGraphs)^*}{\vmlist}} \aslrel
-  \Normal(\overname{\XGraphs}{\vg} \aslsep \overname{\envs}{\newenv}) \cup
+  \evalmultiassignment{\overname{\envs}{\env} \aslsep \overname{\expr^*}{\vlelist} \aslsep \overname{(\vals \times \XGraphs)^*}{\vmlist}} \;\aslrel\;
+  \Normal(\overname{\XGraphs}{\newg} \aslsep \overname{\envs}{\newenv}) \cup
   \overname{\TThrowing}{\ThrowingConfig} \cup \overname{\TError}{\ErrorConfig}
 \]
 evaluates multi-assignments.
 That is, the simultaneous assignment of the list of value-execution graph pairs $\vmlist$
-to the corresponding list of left-hand side expressions $\vlelist$ under the environment $\env$.
+to the corresponding list of left-hand side expressions $\vlelist$, under the environment $\env$.
 The result is either the execution graph $\vg$ and new environment $\newenv$ or an abnormal configuration.
 
+\paragraph{Naming Convention}
+In this chapter, variables containing $\vm$ range over $\vals\times\XGraphs$
+while variables where the $\vm$ is replaced with $\vv$ correspond to their value component.
+For example, $\rmarray\eqname(\rvarray,\vgtwo)$ and $\mindex\eqname(\vindex, \vgone)$.
+
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule{}
+  \inferrule[empty]{}
   {
     \evalmultiassignment{\env, \emptylist, \emptylist} \evalarrow \Normal(\emptygraph, \env)
   }
 \and
-\inferrule{
-  \vlelist \eqname [\vle] + \vlelist'\\
-  \vmlist \eqname [\vm] + \vmlist'\\
-  \evallexpr{\env, \vle, \vm} \evalarrow \Normal(\envp, \vgone) \OrAbnormal\\
-  \evalmultiassignment{\envp, \vlelist', \vmlist'} \evalarrow \Normal(\newenv, \vgtwo) \OrAbnormal\\
-  \vg = \ordered{\vgone}{\aslpo}{\vgtwo}
+\inferrule[nonempty]{
+  \vlelist \eqname [\vle] + \vlelistone\\
+  \vmlist \eqname [\vm] + \vmlistone\\
+  \evallexpr{\env, \vle, \vm} \evalarrow \Normal(\envone, \vgone) \OrAbnormal\\
+  \evalmultiassignment{\envone, \vlelistone, \vmlistone} \evalarrow \Normal(\newenv, \vgtwo) \OrAbnormal\\
+  \newg = \ordered{\vgone}{\aslpo}{\vgtwo}
 }
 {
-  \evalmultiassignment{\env, \vlelist, \vmlist} \evalarrow \Normal(\vg, \newenv)
+  \evalmultiassignment{\env, \vlelist, \vmlist} \evalarrow \Normal(\newg, \newenv)
 }
-
 \end{mathpar}
+Notice that this rule is only defined when the lists $\vlelist$ and $\vmlist$ have the same length,
+which is guaranteed by the rules employing this rule.
+\end{emptyformal}
 
 \section{SemanticsRule.LEDiscard \label{sec:SemanticsRule.LEDiscard}}
-
     \subsection{Prose}
-    Evaluation of the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is $\newenv$ and all
-of the following apply:
+    Evaluation of the left-hand-side expression $\vle$ associated with a
+    value $\vv$ under an environment $\env$ is $\Normal(\newg, \env)$
+    and all of the following apply:
     \begin{itemize}
-    \item \texttt{le} can be discarded;
+    \item $\vle$ can be discarded, that is $\texttt{LE\_Discard}$;
+    \item $\newg$ is $\vg$;
     \item $\newenv$ is $\env$.
     \end{itemize}
 
@@ -3019,23 +3402,26 @@ \section{SemanticsRule.LEDiscard \label{sec:SemanticsRule.LEDiscard}}
 \begin{emptyformal}
   \subsection{Formally}
   \begin{mathpar}
-    \inferrule{\vgp=\vg}
-    { \evallexpr{\env, \texttt{LE\_Discard}, (\vv, \vg)} \evalarrow \Normal(\vgp, \env) }
+    \inferrule{
+      \newg=\vg\\
+      \newenv = \env
+    }
+    { \evallexpr{\env, \texttt{LE\_Discard}, (\vv, \vg)} \evalarrow \Normal(\newg, \newenv) }
   \end{mathpar}
 \end{emptyformal}
 
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.LELocalVar \label{sec:SemanticsRule.LELocalVar}}
-
     \subsection{Prose}
-    Evaluation of the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is $\newenv$ and all
-of the following apply:
+    Evaluation of the left-hand-side expression $\vle$ associated with a
+    value $\vv$ under an environment $\env$ is $\Normal(\newg, \env)$
+    and all of the following apply:
     \begin{itemize}
-    \item \texttt{le} denotes a variable \vx;
-    \item \texttt{x} is locally bound in $\env$;
-    \item $\newenv$ is $\env$ where \texttt{x} is bound to $\vv$.
+    \item $\vle$ denotes a variable $\vx$, that is $\texttt{LE\_Var}(\vx)$;
+    \item $\vx$ is locally bound in $\env$;
+    \item $\newg$ is the ordered composition of $\vg$ and a Write Effect for $\vx$;
+    \item $\newenv$ is $\env$ where $\vx$ is bound to $\vv$ in the local component of the environment.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.LELocalVar.asl}
@@ -3053,25 +3439,25 @@ \section{SemanticsRule.LELocalVar \label{sec:SemanticsRule.LELocalVar}}
       \env \eqname (\tenv, \denv)\\
       \vx \in \dom(L^\denv)\\
       \newenv = (\tenv, (G^\denv, L^\denv[\vx \mapsto \vv]))\\
-      \vg' = \ordered{\vg}{\asldata}{\WriteEffect(\vx)}
+      \newg = \ordered{\vg}{\asldata}{\WriteEffect(\vx)}
     }
-    { \evallexpr{\env, \texttt{LE\_Var}(\vx), (\vv, \vg)} \evalarrow \Normal(\vg',\newenv) }
+    { \evallexpr{\env, \texttt{LE\_Var}(\vx), (\vv, \vg)} \evalarrow \Normal(\newg,\newenv) }
   \end{mathpar}
 \end{emptyformal}
 
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.LEGlobalVar \label{sec:SemanticsRule.LEGlobalVar}}
-
     \subsection{Prose}
-    Evaluation of the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is $\newenv$ and all
-of the following apply:
+    Evaluation of the left-hand-side expression $\vle$ associated with a
+    value $\vv$ under an environment $\env$ is $\Normal(\newg, \env)$
+    and all of the following apply:
     \begin{itemize}
-    \item \texttt{le} denotes a variable \vx;
-    \item \texttt{x} is globally bound in $\env$;
-    \item $\newenv$ is $\env$ where \texttt{x} is bound to $\vv$.
-    \end{itemize}
+      \item $\vle$ denotes a variable $\vx$, that is $\texttt{LE\_Var}(\vx)$;
+      \item $\vx$ is globally bound in $\env$;
+      \item $\newg$ is the ordered composition of $\vg$ and a Write Effect for $\vx$;
+      \item $\newenv$ is $\env$ where $\vx$ is bound to $\vv$ in the global component of the environment.
+      \end{itemize}
 
     \subsection{Example: SemanticsRule.LEGlobalVar.asl}
     In the specification:
@@ -3088,28 +3474,38 @@ \section{SemanticsRule.LEGlobalVar \label{sec:SemanticsRule.LEGlobalVar}}
       \env \eqname (\tenv, \denv)\\
       \vx \in \dom(G^\denv)\\
       \newenv = (\tenv, (G^\denv[\vx \mapsto \vv], L^\denv))\\
-      \vg' = \ordered{\vg}{\asldata}{\WriteEffect(\vx)}
+      \newg = \ordered{\vg}{\asldata}{\WriteEffect(\vx)}
     }
-    { \evallexpr{\env, \texttt{LE\_Var}(\vx), (\vv, \vg)} \evalarrow \Normal(\vg',\newenv) }
+    { \evallexpr{\env, \texttt{LE\_Var}(\vx), (\vv, \vg)} \evalarrow \Normal(\newg,\newenv) }
   \end{mathpar}
 \end{emptyformal}
 
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.LESlice \label{sec:SemanticsRule.LESlice}}
-
-    \subsection{Prose}
-    Evaluation of the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is $\newenv$ and all
-of the following apply:
-    \begin{itemize}
-    \item \texttt{le} denotes a left-hand-side expression sliced as per \texttt{slices};
-    \item The right-hand-side expression corresponding to \texttt{le} is \texttt{re\_bv};
-    \item The evaluation of \texttt{re\_bv} under $\env$ is \texttt{rv\_bv};
-    \item The evaluation of \texttt{slices} under $\env$ is \texttt{positions};
-    \item \texttt{new\_m\_bv} is \texttt{rv\_bv} where the positions \texttt{positions} have been updated to $\vv$;
-    \item $\newenv$ is $\env$ where \texttt{le} is bound to \texttt{new\_m\_bv}.
-    \end{itemize}
+  \subsection{Prose}
+  Evaluation of the left-hand-side expression $\vle$ associated with a
+  value $\vv$ under an environment $\env$ is the output configuration $C$
+  and all of the following apply:
+  \begin{itemize}
+    \item $\vle$ denotes a left-hand-side expression sliced as per $\slices$, \\
+    that is $\texttt{LE\_Slice}(\ebv, \slices)$;
+    \item evaluating the right-hand-side expression that corresponds to $\ebv$
+    (given by applying $\torexpr$ to $\ebv$) under $\env$
+      is either $\Normal(\mbv,\envone)$, \ProseOrAbnormal;
+    \item evaluating $\slices$ under $\envone$ is either $\Normal(\mpositions, \envtwo)$,
+    \ProseOrAbnormal;
+    \item $\mpositions$ consists of the execution graph $\vgone$ and the list of indices $\positions$;
+    \item $\mbv$ consists of the native bitvector $\vbv$ and the execution graph $\vgtwo$;
+    \item writing to the bitvector $\vbv$ at indices $\positions$ using the values from $\vv$
+    is either the updated native bitvector $\vvone$ \ProseOrError;
+    \item $\vgthree$ is the parallel composition of $\vg$, $\vgone$, and $\vgtwo$;
+    \item $\newmbv$ is a pair consisting of $\vvone$ and the execution graph $\vgthree$;
+    \item the steps so far computed the updated bitvector, but have not assigned it to the
+    variable bound to the bitvector given by $\ebv$, which is achieved next.
+    Evaluating the left-hand-side expression $\ebv$ with
+    $\newmbv$ under environment $\envtwo$ is the output configuration $C$,
+  \end{itemize}
 
    \subsection{Example: SemanticsRule.LESlice.asl}
    In the specification:
@@ -3123,16 +3519,16 @@ \section{SemanticsRule.LESlice \label{sec:SemanticsRule.LESlice}}
   \subsection{Formally}
   \begin{mathpar}
     \inferrule{
-      \vm \eqname (\vv, \vg)\\
       \evalexpr{\env, \torexpr(\ebv)} \evalarrow \Normal(\mbv,\envone) \OrAbnormal\\
       \evalslices{\envone, \slices} \evalarrow \Normal(\mpositions, \envtwo) \OrAbnormal\\
       \mpositions \eqname (\vgone, \positions)\\
-      \vbv \eqname (\mbv, \vgtwo)\\\\
-      \writetobitvector(\positions, \vv, \vbv) \evalarrow \vv' \terminateas \Error\\
-      \vg' = \vg \parallel \vgone \parallel \vgtwo\\
-      \evallexpr{\env, \texttt{LE\_Slice}(\ebv, \slices), (\vv', \vg')} \evalarrow C
+      \mbv \eqname (\vbv, \vgtwo)\\\\
+      \writetobitvector(\positions, \vv, \vbv) \evalarrow \vvone \terminateas \Error\\
+      \vgthree = \vg \parallel \vgone \parallel \vgtwo\\
+      \newmbv = (\vvone, \vgthree)\\
+      \evallexpr{\envtwo, \ebv, \newmbv} \evalarrow C
     }
-    { \evallexpr{\envtwo, \texttt{LE\_Slice}(\ebv), \vm} \evalarrow C }
+    { \evallexpr{\envtwo, \texttt{LE\_Slice}(\ebv, \slices), (\vv, \vg)} \evalarrow C }
   \end{mathpar}
 \end{emptyformal}
 
@@ -3142,18 +3538,24 @@ \subsection{Comments}
 \section{SemanticsRule.LESetArray \label{sec:SemanticsRule.LESetArray}}
 
     \subsection{Prose}
-    Evaluation of the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is $\newenv$ and all
-of the following apply:
+    Evaluation of the left-hand-side expression $\vle$ associated with a
+    value $\vv$ under an environment $\env$ is the output configuration $C$
+    and all of the following apply:
     \begin{itemize}
-    \item \texttt{le} denotes an array \texttt{le\_array} and an index \texttt{e\_index};
-    \item The right-hand-side expression corresponding to \texttt{le\_array} is \texttt{re\_array};
-    \item The evaluation of \texttt{re\_array} under $\env$ is \texttt{rv\_array};
-    \item The evaluation of \texttt{e\_index} under $\env$ is \texttt{v\_index};
-    \item \texttt{new\_v\_array} is \texttt{rv\_array} where the value at index \texttt{v\_index} has been
-      updated to $\vv$;
-    \item $\newenv$ is $\env$ where \texttt{le\_array} is bound to
-      \texttt{new\_v\_array}.
+    \item $\vle$ denotes an array $\rearray$ and an index $\eindex$,
+    that is \\ $\texttt{LE\_SetArray}(\rearray, \eindex)$;
+    \item evaluating the right-hand-side expression corresponding to $\rearray$ under $\env$
+    is either \Normal(\rmarray, \envone), \ProseOrAbnormal;
+    \item evaluating $\eindex$ under $\envone$ is either \Normal(\mindex, \envtwo), \ProseOrAbnormal;
+    \item $\mindex$ consists of the native integer $\vindex$ and the execution graph $\vgone$;
+    \item $\vindex$ is the native integer for $\vi$;
+    \item $\rmarray$ consists of the native vector $\rvarray$ and the execution graph $\vgtwo$;
+    \item setting the value $\vv$ at index $\vi$ of $\rvarray$ is the native vector $\vvone$;
+    \item $\vmone$ is the pair consisting of $\vvone$ and the parallel composition of $\vgone$ and $\vgtwo$;
+    \item the steps so far computed the updated array, but have not assigned it to the variable
+    bound to the array given by $\rearray$, which is achieved next.
+    Evaluating the left-hand-side expression $\rearray$ under environment $\envtwo$ with $\vmone$
+    is the output configuration $C$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.LESetArray.asl}
@@ -3168,40 +3570,44 @@ \section{SemanticsRule.LESetArray \label{sec:SemanticsRule.LESetArray}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \vm \eqname (\vv, \vg)\\
     \evalexpr{\env, \torexpr(\rearray)} \evalarrow \Normal(\rmarray, \envone) \OrAbnormal\\
     \evalexpr{\envone, \eindex} \evalarrow \Normal(\mindex, \envtwo) \OrAbnormal\\
     \mindex \eqname (\vindex, \vgone)\\
     \vindex \eqname \nvint(\vi)\\
     \rmarray \eqname (\rvarray, \vgtwo)\\
-    \setindex(\vi, \vv, \rvarray) \evalarrow \vv'\\
-    \vm' \eqname (\vv', \vgone \parallel \vgtwo)\\
-    \evallexpr{\envtwo, \rearray, \vm'} \evalarrow C
+    \setindex(\vi, \vv, \rvarray) \evalarrow \vvone\\
+    \vmone = (\vvone, \vgone \parallel \vgtwo)\\
+    \evallexpr{\envtwo, \rearray, \vmone} \evalarrow C
   }
-  { \evallexpr{\env, \texttt{LE\_SetArray}(\rearray, \eindex), \vm} \evalarrow C }
+  { \evallexpr{\env, \texttt{LE\_SetArray}(\rearray, \eindex), (\vv, \vg)} \evalarrow C }
 \end{mathpar}
 \end{emptyformal}
 
 \subsection{Comments}
   This is related to \identr{WHRS}.
 
-
 \section{SemanticsRule.LESetField \label{sec:SemanticsRule.LESetField}}
 
-    \subsection{Prose}
-    Evaluation of the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is $\newenv$ and all
-of the following apply:
+  \subsection{Prose}
+    Evaluation of the left-hand-side expression $\vle$ associated with a
+    value $\vv$ under an environment $\env$ is the output configuration $C$
+    and all of the following apply:
     \begin{itemize}
-    \item \texttt{le} denotes a field name \texttt{field\_name} in a record \texttt{le\_record};
-    \item The right-hand-side expression corresponding to \texttt{le\_record} is
-      \texttt{re\_record};
-    \item The evaluation of \texttt{re\_record} under $\env$ is \texttt{rv\_record};
-    \item \texttt{new\_v\_record} is \texttt{rv\_record} where the field \texttt{field\_name} has been
-      updated to $\vv$;
-    \item $\newenv$ is $\env$ where \texttt{le\_record} is bound to
-      \texttt{new\_v\_record}.
-    \end{itemize}
+    \item $\vle$ denotes a field name $\fieldname$ in a record \texttt{le\_record},
+    that is \\ $\texttt{LE\_SetField}(\rerecord, \fieldname)$;
+    \item evaluating the right-hand-side expression corresponding to $\rerecord$
+    under $\env$ is either $\Normal(\rmrecord, \envone)$ \ProseOrAbnormal
+    \item $\rmrecord$ is a pair consisting of the native record $\rvrecord$ and
+    the execution graph $\vgone$;
+    \item setting the field $\fieldname$ in the native record $\rvrecord$ to $\vv$
+    is the updated native record $\vvone$;
+    \item $\vmone$ is the pair consisting of the native vector $\vvone$ and the
+    execution graph that is the parallel composition of $\vg$ and $\vgone$;
+    \item the steps so far computed the updated record, but have not assigned it to
+    the variable holding the record given by $\record$, which is achieved next.
+    Evaluating the left-hand-side expression $\rerecord$ under environment $\envone$ with $\vmone$
+    is the output configuration $C$.
+  \end{itemize}
 
     \subsection{Example: SemanticsRule.LESetField.asl}
     In the specification:
@@ -3215,31 +3621,34 @@ \section{SemanticsRule.LESetField \label{sec:SemanticsRule.LESetField}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \vm \eqname (\vv, \vg)\\
     \evalexpr{\env, \torexpr(\rerecord)} \evalarrow \Normal(\rmrecord, \envone) \OrAbnormal\\
     \rmrecord \eqname (\rvrecord, \vgone)\\
-    \setfield(\fieldname, \vv, \rvrecord) \evalarrow \vv'\\
-    \vm' = (\vv', \vg \parallel \vgone)\\
-    \evallexpr{\env1, \rerecord, \vm'} \evalarrow C
+    \setfield(\fieldname, \vv, \rvrecord) \evalarrow \vvone\\
+    \vmone = (\vvone, \vg \parallel \vgone)\\
+    \evallexpr{\env1, \rerecord, \vmone} \evalarrow C
   }
-  { \evallexpr{\env, \texttt{LE\_SetField}(\rerecord, \fieldname), \vm} \evalarrow C }
+  { \evallexpr{\env, \texttt{LE\_SetField}(\rerecord, \fieldname), (\vv, \vg)} \evalarrow C }
 \end{mathpar}
 \end{emptyformal}
 
 \subsection{Comments}
   This is related to \identr{WHRS}.
 
-
 \section{SemanticsRule.LEDestructuring \label{sec:SemanticsRule.LEDestructuring}}
-
     \subsection{Prose}
-    Evaluation of the left-hand-side expression \texttt{le} associated with a
-value $\vv$ under an environment $\env$ is $\newenv$ and all
-of the following apply:
+    Evaluation of the left-hand-side expression $\vle$ associated with a
+    native vector $\vv$ under an environment $\env$ is the output configuration $C$
+    and all of the following apply:
     \begin{itemize}
-    \item \texttt{le} denotes a list of left-hand-side expressions \texttt{le\_list};
-    \item $\newenv$ is $\env$ where each left-hand-side expression in \texttt{le\_list} has
-      been assigned the value at the corresponding index in $\vv$.
+    \item $\vle$ denotes a list of left-hand-side expressions $\vlelist$,
+    that is \\ $\texttt{LE\_Destructuring}(\vlelist)$;
+    \item $\vlelist$ is the list of expressions $\vle_{1..k}$;
+    \item getting the values from the native vector $\vv$ at each index $i=1..k$
+    results in $\vv_{i=1..k}$;
+    \item $\nmonads$ is the list of pairs consisting of $\vv_i$ and $\vg$ for $i=1..k$;
+    \item evaluating the multi-assignment between $\vlelist$ and the list $\nmonads$
+    under $\env$ achieves the effects of assigning each value to the respective
+    subexpressions, resulting in the output configuration $C$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.LEDestructuring.asl}
@@ -3254,13 +3663,12 @@ \section{SemanticsRule.LEDestructuring \label{sec:SemanticsRule.LEDestructuring}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \vm \eqname (\vv, \vg)\\
-    \vlelist = [\vle_{1..k}]\\
+    \vlelist \eqname [\vle_{1..k}]\\
     i=1..k: \getindex(i, \vv) \evalarrow \vv_i\\
     \nmonads = [i=1..k: (\vv_i, \vg)]\\
     \evalmultiassignment{\env, \vlelist, \nmonads} \evalarrow C
   }
-  { \evallexpr{\env, \texttt{LE\_Destructuring}(\vlelist), \vm} \evalarrow C }
+  { \evallexpr{\env, \texttt{LE\_Destructuring}(\vlelist), (\vv, \vg)} \evalarrow C }
 \end{mathpar}
 \end{emptyformal}
 
@@ -3270,48 +3678,102 @@ \section{SemanticsRule.LEDestructuring \label{sec:SemanticsRule.LEDestructuring}
 \chapter{Evaluation of Slices \label{chap:eval_slices}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+The rule for evaluating a list of slices is
+SemanticsRule.Slices (see \secref{SemanticsRule.Slices}).
+
+The relation for evaluating a single slice is
+\[
+  \begin{array}{rl}
+  \evalslice{\overname{\envs}{\env} \times \overname{\slice}{\vs}} \;\aslrel &
+    \Normal(((\overname{\tint}{\vstart} \times \overname{\tint}{\vlength}) \times \overname{\XGraphs}{\newg}), \overname{\envs}{\newenv})\ \cup \\
+    & \overname{\Throwing}{\ThrowingConfig} \cup \overname{\TError}{\ErrorConfig}
+  \end{array}
+\]
+where a single slice $\vs$ is evaluated under environment $\env$ is,
+resulting either in $\Normal(((\vstart, \vlength), \vg), \newenv)$
+or an error configuration,
+and one of the following applies:
+\begin{itemize}
+  \item SemanticsRule.SliceSingle (see \secref{SemanticsRule.SliceSingle}),
+  \item SemanticsRule.SliceLength (see \secref{SemanticsRule.SliceLength}),
+  \item SemanticsRule.SliceRange (see \secref{SemanticsRule.SliceRange}),
+  \item SemanticsRule.SliceStar (see \secref{SemanticsRule.SliceStar}).
+  \end{itemize}
+
+\section{SemanticsRule.Slices \label{sec:SemanticsRule.Slices}}
+\subsection{Prose}
+The relation
+\[
+  \begin{array}{rl}
+  \evalslices{\overname{\envs}{\env} \times \overname{\slice^*}{\slices}} \;\aslrel &
+    \Normal((\overname{(\vals \times \vals)^*}{\ranges} \times \overname{\XGraphs}{\newg}), \overname{\envs}{\newenv})\ \cup \\
+    & \overname{\Throwing}{\ThrowingConfig} \cup \overname{\TError}{\ErrorConfig}
+  \end{array}
+\]
+evalutes a list of slices $\slices$ under environment $\env$, resulting in either
+$\Normal((\ranges, \newg), \newenv)$ or an abnormal configuration,
+and one of the following applies:
+\begin{itemize}
+  \item All of the following apply (\textsc{empty}):
+  \begin{itemize}
+    \item the list of slices is empty;
+    \item $\ranges$ is the empty list;
+    \item $\newg$ is the empty graph;
+    \item $\newenv$ is $\env$;
+  \end{itemize}
+
+  \item All of the following apply (\textsc{nonempty}):
+  \begin{itemize}
+    \item the list of slices has $\slice$ as the head and $\slicesone$ as the tail;
+    \item evaluating the slice $\vslice$ under $\env$ either results in \\
+    $\Normal((\range, \vgone), \envone)$     \ProseOrAbnormal;
+    \item evaluating the tail list $\slicesone$ under $\envone$ either results in \\
+    $\Normal((\rangesone, \vgtwo), \newenv)$ \ProseOrAbnormal;
+    \item $\ranges$ is the the concatenation of $\range$ to $\rangesone$;
+    \item $\newg$ is the parallel composition of $\vgone$ and $\vgtwo$.
+  \end{itemize}
+\end{itemize}
+
 \texttt{eval\_slices env slices} is the list of pair \texttt{(start\_n, length\_n)} that
 corresponds to the start (included) and the length of each slice in
-\texttt{slices}.
+$\slices$.
 
-We define evaluation of a list of slices in terms of the following rules,
-which make use of the rules for evaluating a single slice, in the sequel of this chapter:
+\subsection{Code}
+\VerbatimInput[firstline=\SlicesBegin, lastline=\SlicesEnd]{../Interpreter.ml}
+
+\begin{emptyformal}
+\subsection{Formally}
 \begin{mathpar}
-  \inferrule{}
+  \inferrule[empty]{}
   {
     \evalslices{\env, \emptylist} \evalarrow \Normal((\emptylist, \emptygraph), \env)
   }
   \and
-  \inferrule{
-    \evalslice{\env, \slice} \evalarrow \Normal((\range, \vgone), \envone) \OrAbnormal\\
-    \evalslices{\envone, \slices} \evalarrow \Normal((\ranges, \vgtwo), \newenv) \OrAbnormal\\
+  \inferrule[nonempty]{
+    \slices \eqname [\vslice] + \slicesone\\
+    \evalslice{\env, \vslice} \evalarrow \Normal((\range, \vgone), \envone) \OrAbnormal\\
+    \evalslices{\envone, \slicesone} \evalarrow \Normal((\rangesone, \vgtwo), \newenv) \OrAbnormal\\
+    \ranges = [\range] + \rangesone\\
+    \newg = \vgone \parallel \vgtwo
   }
   {
-    \evalslices{\env, \slice + \slices} \evalarrow \Normal([\range] + \ranges, \vgone \parallel \vgtwo), \newenv)
+    \evalslices{\env, \slices} \evalarrow \Normal((\ranges, \newg), \newenv)
   }
 \end{mathpar}
+\end{emptyformal}
 
-Evaluation of a single slice \texttt{s} under environment $\env$ is
-\texttt{((start, length), new\_env)}, or an error, and one of the following applies:
-\begin{itemize}
-\item SemanticsRule.SliceSingle (see Section~\ref{sec:SemanticsRule.SliceSingle}),
-\item SemanticsRule.SliceLength (see Section~\ref{sec:SemanticsRule.SliceLength}),
-\item SemanticsRule.SliceRange (see Section~\ref{sec:SemanticsRule.SliceRange}),
-\item SemanticsRule.SliceStar (see Section~\ref{sec:SemanticsRule.SliceStar}).
-\end{itemize}
+\isempty{\subsection{Comments}}
 
 \section{SemanticsRule.SliceSingle \label{sec:SemanticsRule.SliceSingle}}
-
   \subsection{Prose}
-  The result of evaluation is \texttt{((start, length), new\_env)} and all
-of the following apply:
+  evaluating the slice $\vs$ under environment $\env$ is either \\
+  $\Normal(((\start, \vlength), \vg), \newenv)$
+  or an abnormal configuration and all of the following apply:
   \begin{itemize}
-    \item \texttt{s} is the single expression $\ve$;
-    \item \texttt{start} is the result of evaluation of the expression~$\ve$
-      in the environment $\env$;
-    \item $\newenv$ is the environment $\env$ modified after
-      evaluation of the expression~$\ve$;
-    \item \texttt{length} is the integer value 1.
+    \item $\vs$ is the single expression $\ve$, that is $\texttt{Slice\_Single}(\ve)$;
+    \item evaluating $\ve$ under $\env$ either results in \Normal((\vstart, \newg), \newenv)
+    \ProseOrAbnormal;
+    \item $\vlength$ is the integer value 1.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.SliceSingle.asl}
@@ -3327,10 +3789,11 @@ \section{SemanticsRule.SliceSingle \label{sec:SemanticsRule.SliceSingle}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evallexpr{\env, \ve} \evalarrow \Normal((\start, \vg), \newenv) \OrAbnormal\\
+    \evalexpr{\env, \ve} \evalarrow \Normal((\vstart, \newg), \newenv) \OrAbnormal\\
+    \vlength = \nvint(1)
   }
   {
-    \evalslice{\env, \texttt{Slice\_Single}(\ve)} \evalarrow \Normal(((\start, \nvint(1)), \vg), \newenv)
+    \evalslice{\env, \texttt{Slice\_Single}(\ve)} \evalarrow \Normal(((\vstart, \vlength), \newg), \newenv)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3338,20 +3801,18 @@ \section{SemanticsRule.SliceSingle \label{sec:SemanticsRule.SliceSingle}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.SliceLength \label{sec:SemanticsRule.SliceLength}}
-
   \subsection{Prose}
-  The result of evaluation is \texttt{((start, length), new\_env)} and all of the following
-apply:
+  evaluating the slice $\vs$ under environment $\env$ is either \\
+  $\Normal(((\start, \vlength), \vg), \newenv)$
+  or an abnormal configuration and all of the following apply:
   \begin{itemize}
-    \item \texttt{s} is the slice which starts at expression~\texttt{e\_start} with length~\texttt{e\_length};
-    \item \texttt{start} is the result of evaluation of the
-      expression~\texttt{e\_start} in the environment $\env$;
-    \item \texttt{env\_1} is the environment $\env$ modified after
-      evaluation of the expression~\texttt{e\_start};
-    \item \texttt{length} is the result of evaluation of the
-      expression~\texttt{e\_length} in the environment \texttt{env\_1};
-    \item $\newenv$ is the environment \texttt{env\_1} modified after
-      evaluation of the expression~\texttt{e\_length}.
+    \item $\vs$ is the slice which starts at expression~$\estart$ with length~$\elength$,
+    that is $\texttt{Slice\_Length}(\estart, \elength)$;
+    \item evaluating $\estart$ under $\env$ is either \Normal(\mstart, \envone) \ProseOrAbnormal;
+    \item evaluating $\elength$ under $\envone$ is either \Normal(\mlength, \newenv) \ProseOrAbnormal;
+    \item $\mstart$ is a pair consisting of the native integer $\vstart$ and execution graph $\vgone$;
+    \item $\mlength$ is a pair consisting of the native integer $\vlength$ and execution graph $\vgtwo$;
+    \item $\newg$ is the parallel composition of $\vgone$ and $\vgtwo$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.SliceLength.asl}
@@ -3366,14 +3827,14 @@ \section{SemanticsRule.SliceLength \label{sec:SemanticsRule.SliceLength}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evallexpr{\env, \estart} \evalarrow \Normal(\mstart, \envone) \OrAbnormal\\
-    \evallexpr{\envone, \elength} \evalarrow \Normal(\mlength, \newenv) \OrAbnormal\\
-    \mstart \eqname (\vstart, \vgone)\\
-    \mlength \eqname (\vlength, \vgtwo)\\
-    \vg = \vgone \parallel \vgtwo
+    \evalexpr{\env, \estart} \evalarrow \Normal(\mstart, \envone) \OrAbnormal\\
+    \evalexpr{\envone, \elength} \evalarrow \Normal(\mlength, \newenv) \OrAbnormal\\
+    \mstart = (\vstart, \vgone)\\
+    \mlength = (\vlength, \vgtwo)\\
+    \newg = \vgone \parallel \vgtwo
   }
   {
-    \evalslice{\env, \texttt{Slice\_Length}(\estart, \elength)} \evalarrow \\ \Normal(((\vstart, \vlength), \vg), \newenv)
+    \evalslice{\env, \texttt{Slice\_Length}(\estart, \elength)} \evalarrow \\ \Normal(((\vstart, \vlength), \newg), \newenv)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3381,21 +3842,19 @@ \section{SemanticsRule.SliceLength \label{sec:SemanticsRule.SliceLength}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.SliceRange \label{sec:SemanticsRule.SliceRange}}
-
   \subsection{Prose}
-  The result of evaluation is \texttt{((start, length), new\_env)} and all of the following apply:
+  evaluating the slice $\vs$ under environment $\env$ is either \\
+  $\Normal(((\start, \vlength), \vg), \newenv)$
+  or an abnormal configuration and all of the following apply:
   \begin{itemize}
-    \item \texttt{s} is the slice range between the
-      expressions~\texttt{e\_start} and~\texttt{e\_top};
-    \item \texttt{v\_top} is the result of evaluation of the
-      expression~\texttt{e\_top} in the environment $\env$;
-    \item \texttt{env\_1} is the environment $\env$ modified after
-      evaluation of the expression~\texttt{e\_top};
-    \item \texttt{start} is the result of evaluation of the
-      expression~\texttt{e\_start} in the environment \texttt{env\_1};
-    \item $\newenv$ is the environment \texttt{env\_1} modified after
-      evaluation of the expression~\texttt{e\_start};
-    \item \texttt{length} is the integer value \texttt{(vtop - start) + 1};
+    \item $\vs$ is the slice range between the
+      expressions $\estart$ and $\etop$, that is $\texttt{Slice\_Range}(\etop, \estart)$;
+    \item evaluating $\etop$ under $\env$ is either $\Normal(\mtop, \envone)$ \ProseOrAbnormal;
+    \item $\mtop$ is a pair consisting of the native integer $\vvtop$ and execution graph $\vgone$;
+    \item evaluating $\estart$ under $\envone$ is either $\Normal(\mstart, \newenv)$ \ProseOrAbnormal;
+    \item $\mstart$ is a pair consisting of the native integer $\vstart$ and execution graph $\vgtwo$;
+    \item $\vlength$ is the integer value \texttt{(v\_top - v\_start) + 1};
+    \item $\newg$ is the parallel composition of $\vgone$ and $\vgtwo$.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.SliceRange.asl}
@@ -3410,15 +3869,16 @@ \section{SemanticsRule.SliceRange \label{sec:SemanticsRule.SliceRange}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evallexpr{\env, \etop} \evalarrow \Normal(\mtop, \envone) \OrAbnormal\\
+    \evalexpr{\env, \etop} \evalarrow \Normal(\mtop, \envone) \OrAbnormal\\
     \mtop \eqname (\vvtop, \vgone)\\
-    \evallexpr{\envone, \estart} \evalarrow \Normal(\mstart, \newenv) \OrAbnormal\\
+    \evalexpr{\envone, \estart} \evalarrow \Normal(\mstart, \newenv) \OrAbnormal\\
     \mstart \eqname (\vstart, \vgtwo)\\
-    \binop(\PLUS, \nvint(1), \binop(\MINUS, \vvtop, \vstart)) \evalarrow \length\\
-    \vg = \vgone \parallel \vgtwo
+    \binop(\MINUS, \vvtop, \vstart) \evalarrow \vdiff\\
+    \binop(\PLUS, \nvint(1), \vdiff) \evalarrow \vlength\\
+    \newg = \vgone \parallel \vgtwo
   }
   {
-    \evalslice{\env, \texttt{Slice\_Range}(\etop, \estart)} \evalarrow \\ \Normal(((\start, \length), \vg), \newenv)
+    \evalslice{\env, \texttt{Slice\_Range}(\etop, \estart)} \evalarrow \\ \Normal(((\vstart, \vlength), \newg), \newenv)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3426,25 +3886,21 @@ \section{SemanticsRule.SliceRange \label{sec:SemanticsRule.SliceRange}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.SliceStar \label{sec:SemanticsRule.SliceStar}}
-
   \subsection{Prose}
-  The result of evaluation is \texttt{((start, length), new\_env)} and all of the following
-apply:
+  evaluating the slice $\vs$ under environment $\env$ is either \\
+  $\Normal(((\start, \vlength), \vg), \newenv)$
+  or an abnormal configuration and all of the following apply:
   \begin{itemize}
-    \item \texttt{s} is the slice with factor given by the
-      expression~\texttt{e\_factor} and length given by the
-      expression~\texttt{e\_length};
-    \item \texttt{v\_factor} is the result of evaluation of the
-      expression~\texttt{e\_factor} in the environment $\env$;
-    \item \texttt{env\_1} is the environment $\env$ modified after
-      evaluation of the expression~\texttt{e\_factor};
-    \item \texttt{length} is the result of evaluation of the
-      expression~\texttt{e\_length} in the environment \texttt{env\_1};
-    \item $\newenv$ is the environment \texttt{env\_1} modified after
-      evaluation of the expression~\texttt{e\_length};
-    \item \texttt{start} is the integer value
-      $\texttt{v\_factor} \times \texttt{length}$.
-  \end{itemize}
+    \item $\vs$ is the slice with factor given by the
+      expression $\efactor$ and length given by the
+      expression $\elength$, that is $\texttt{Slice\_Star}(\efactor, \elength)$;
+    \item evaluating $\efactor$ under $\env$ is either $\Normal(\mfactor, \envone)$ \ProseOrAbnormal;
+    \item $\mfactor$ is a pair consisting of the native integer $\vfactor$ and execution graph $\vgone$;
+    \item evaluating $\elength$ under $\env$ is either $\Normal(\mlength, \newenv)$ \ProseOrAbnormal;
+    \item $\mlength$ is a pair consisting of the native integer $\vlength$ and execution graph $\vgtwo$;
+    \item $\vstart$ is the native integer $\vfactor \times \vlength$;
+   \item $\newg$ is the parallel composition of $\vgone$ and $\vgtwo$.
+   \end{itemize}
 
 
   \subsection{Example: SemanticsRule.SliceStar.asl}
@@ -3459,15 +3915,15 @@ \section{SemanticsRule.SliceStar \label{sec:SemanticsRule.SliceStar}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evallexpr{\env, \efactor} \evalarrow \Normal(\mfactor, \envone) \OrAbnormal\\
+    \evalexpr{\env, \efactor} \evalarrow \Normal(\mfactor, \envone) \OrAbnormal\\
     \mfactor = (\vfactor, \vgone)\\
-    \evallexpr{\envone, \elength} \evalarrow \Normal(\mlength, \newenv) \OrAbnormal\\
+    \evalexpr{\envone, \elength} \evalarrow \Normal(\mlength, \newenv) \OrAbnormal\\
     \mlength = (\vlength, \vgtwo)\\
-    \binop(\texttt{"*"}, \vfactor, \vlength) \evalarrow \length \\
-    \vg = \vgone \parallel \vgtwo
+    \binop(\MUL, \vfactor, \vlength) \evalarrow \vstart \\
+    \newg = \vgone \parallel \vgtwo
   }
   {
-    \evalslice{\env, \texttt{Slice\_Star}(\efactor, \elength)} \evalarrow \\ \Normal(((\start, \length), \vg), \newenv)
+    \evalslice{\env, \texttt{Slice\_Star}(\efactor, \elength)} \evalarrow \\ \Normal(((\vstart, \vlength), \newg), \newenv)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3478,32 +3934,35 @@ \section{SemanticsRule.SliceStar \label{sec:SemanticsRule.SliceStar}}
 \chapter{Evaluation of Patterns \label{chap:eval_pattern}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\texttt{eval\_pattern env pos v p} determines if $\vv$ matches the pattern $\vp$.
-
-Evaluation of the pattern $\vp$ under environment $\env$ with
-respect to value $\vv$ is \texttt{b}, or an error, and one of the
-following applies:
+The relation
+\[
+  \evalpattern{\overname{\envs}{\env} \times \overname{\vals}{\vv} \times \overname{\pattern}{\vp}} \;\aslrel\;
+  \Normal(\overname{\tbool}{\vb}, \overname{\XGraphs}{\newg})
+\]
+determines whether a value $\vv$ matches the pattern $\vp$ under environment $\env$
+resulting in either $\Normal(\vb, \newg)$ or an abnormal configuration,
+and one of the following applies:
 \begin{itemize}
-\item SemanticsRule.PAll (see Section~\ref{sec:SemanticsRule.PAll})
-\item SemanticsRule.PAny (see Section~\ref{sec:SemanticsRule.PAny})
-\item SemanticsRule.PGeq (see Section~\ref{sec:SemanticsRule.PGeq})
-\item SemanticsRule.PLeq (see Section~\ref{sec:SemanticsRule.PLeq})
-\item SemanticsRule.PNot (see Section~\ref{sec:SemanticsRule.PNot})
-\item SemanticsRule.PRange (see Section~\ref{sec:SemanticsRule.PRange})
-\item SemanticsRule.PSingle (see Section~\ref{sec:SemanticsRule.PSingle})
-\item SemanticsRule.PMask (see Section~\ref{sec:SemanticsRule.PMask})
-\item SemanticsRule.PTuple (see Section~\ref{sec:SemanticsRule.PTuple})
+\item SemanticsRule.PAll (see \secref{SemanticsRule.PAll})
+\item SemanticsRule.PAny (see \secref{SemanticsRule.PAny})
+\item SemanticsRule.PGeq (see \secref{SemanticsRule.PGeq})
+\item SemanticsRule.PLeq (see \secref{SemanticsRule.PLeq})
+\item SemanticsRule.PNot (see \secref{SemanticsRule.PNot})
+\item SemanticsRule.PRange (see \secref{SemanticsRule.PRange})
+\item SemanticsRule.PSingle (see \secref{SemanticsRule.PSingle})
+\item SemanticsRule.PMask (see \secref{SemanticsRule.PMask})
+\item SemanticsRule.PTuple (see \secref{SemanticsRule.PTuple})
 \end{itemize}
 
 \section{SemanticsRule.PAll \label{sec:SemanticsRule.PAll}}
-
   \subsection{Prose}
-  Evaluation of the pattern $\vp$ under environment $\env$ with
-  respect to value $\vv$ is \texttt{b} and all of the following apply:
+  evaluation of the pattern $\vp$ under environment $\env$ with
+  respect to value $\vv$ is $\Normal(\vb, \newg)$ and all of the following apply:
   \begin{itemize}
-    \item $\vp$ is the pattern which matches everything, and therefore
+    \item $\vp$ is the pattern which matches everything, that is $\texttt{Pattern\_All}$, and therefore
       matches $\vv$;
-    \item \texttt{b} is the boolean value \texttt{true}.
+    \item $\vb$ is the native boolean value \True;
+    \item $\newg$ is the empty graph.
   \end{itemize}
 
   \subsection{Example: SemanticsRule.PAll.asl}
@@ -3525,14 +3984,16 @@ \section{SemanticsRule.PAll \label{sec:SemanticsRule.PAll}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.PAny \label{sec:SemanticsRule.PAny}}
-
     \subsection{Prose}
-  Evaluation of the pattern $\vp$ under environment $\env$ with
-  respect to value $\vv$ is \texttt{b} and all of the following apply:
+    evaluation of the pattern $\vp$ under environment $\env$ with
+    respect to value $\vv$ is either $\Normal(\vb, \newg)$ or an abnormal configuration,
+    and all of the following apply:
     \begin{itemize}
-      \item $\vp$ is a list of patterns \texttt{ps};
-      \item \texttt{bs} is the list resulting of the evaluation of the patterns in \texttt{ps} under environment $\env$ with respect to value $\vv$;
-      \item \texttt{b} is the disjunction of the values in \texttt{bs}.
+      \item $\vp$ is a list of patterns $\vps$, that is $\texttt{Pattern\_Any}(\vps)$;
+      \item $\vps$ is $\vp_{1..k}$;
+      \item evaluating each pattern $\vp_i$ under $\env$ either results in $\Normal(\nvbool(\vb_i), \vg_i)$ \ProseOrAbnormal;
+      \item $\vb$ is the native Boolean that is the disjunction of $\vb_i$, for $i=1..k$;
+      \item $\newg$ is the parallel composition of all execution graphs $\vg_i$, for $i=1..k$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.PAnyTRUE.asl}
@@ -3550,11 +4011,11 @@ \section{SemanticsRule.PAny \label{sec:SemanticsRule.PAny}}
   \inferrule{
     \vps \eqname \vp_{1..k}\\
     i=1..k : \evalpattern{\env, \vv, \vp_i} \evalarrow \Normal(\nvbool(\vb_i), \vg_i) \terminateas \ErrorConfig\\
-    \vv = \nvbool(\bigvee_{i=1..k} \vb_i)\\
-    \vg = \vg_1 \parallel \ldots \parallel \vg_k
+    \vb = \nvbool(\bigvee_{i=1..k} \vb_i)\\
+    \newg = \vg_1 \parallel \ldots \parallel \vg_k
   }
   {
-    \evalpattern{\env, \vv, \texttt{Pattern\_Any}(\vps)} \evalarrow \Normal(\vv, \vg)
+    \evalpattern{\env, \vv, \texttt{Pattern\_Any}(\vps)} \evalarrow \Normal(\vb, \newg)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3562,17 +4023,17 @@ \section{SemanticsRule.PAny \label{sec:SemanticsRule.PAny}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.PGeq \label{sec:SemanticsRule.PGeq}}
-
     \subsection{Prose}
-    Evaluation of the pattern $\vp$ under environment $\env$ with
-    respect to value $\vv$ is \texttt{b} and all of the following apply:
+    evaluation of the pattern $\vp$ under environment $\env$ with
+    respect to value $\vv$ is either $\Normal(\vb, \newg)$ or an error configuration,
+    and all of the following apply:
     \begin{itemize}
       \item $\vp$ is the condition corresponding to being greater or equal
-        than the side-effect-free expression $\ve$;
-      \item \texttt{v'} is the side-effect-free evaluation of $\ve$ in
-        $\env$;
-      \item \texttt{b} is the boolean value corresponding to whether $\vv$
-        is greater or equal to \texttt{v'}.
+        than the side-effect-free expression $\ve$, that is $\texttt{Pattern\_Geq}(\ve)$;
+      \item the side-effect-free evaluation of $\ve$ is either
+      $\Normal(\vvone, \newg)$ \ProseOrError;
+      \item $\vb$ is the Boolean value corresponding to whether $\vv$
+        is greater or equal to $\vvone$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.PGeqTRUE.asl}
@@ -3588,10 +4049,11 @@ \section{SemanticsRule.PGeq \label{sec:SemanticsRule.PGeq}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexprsef{\env, \ve} \evalarrow \Normal(\vv', \vg) \terminateas \ErrorConfig
+    \evalexprsef{\env, \ve} \evalarrow \Normal(\vvone, \newg) \terminateas \ErrorConfig\\
+    \binop(\GEQ, \vv, \vvone) \evalarrow \vb
   }
   {
-    \evalpattern{\env, \vv, \texttt{Pattern\_Geq}(\ve)} \evalarrow \Normal(\binop(\GEQ, \vv, \vv'), \vg)
+    \evalpattern{\env, \vv, \texttt{Pattern\_Geq}(\ve)} \evalarrow \Normal(\vb, \newg)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3599,18 +4061,18 @@ \section{SemanticsRule.PGeq \label{sec:SemanticsRule.PGeq}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.PLeq \label{sec:SemanticsRule.PLeq}}
-
-    \subsection{Prose}
-    Evaluation of the pattern $\vp$ under environment $\env$ with
-    respect to value $\vv$ is \texttt{b} and all of the following apply:
-    \begin{itemize}
-      \item $\vp$ is the condition corresponding to being less or equal
-        than the side-effect-free expression $\ve$;
-      \item \texttt{v'} is the side-effect-free evaluation of $\ve$ in
-        $\env$;
-      \item \texttt{b} is the boolean value corresponding to whether $\vv$
-        is less or equal to \texttt{v'}.
-    \end{itemize}
+  \subsection{Prose}
+  evaluation of the pattern $\vp$ under environment $\env$ with
+  respect to value $\vv$ is either $\Normal(\vb, \newg)$ or an error configuration,
+  and all of the following apply:
+  \begin{itemize}
+    \item $\vp$ is the condition corresponding to being less or equal
+      than the side-effect-free expression $\ve$, that is $\texttt{Pattern\_Leq}(\ve)$;
+    \item the side-effect-free evaluation of $\ve$ is either
+    $\Normal(\vvone, \newg)$ \ProseOrError;
+    \item $\vb$ is the Boolean value corresponding to whether $\vv$
+      is less or equal to $\vvone$.
+  \end{itemize}
 
     \subsection{Example: SemanticsRule.PLeqTRUE.asl}
     \VerbatimInput{../tests/ASLSemanticsReference.t/SemanticsRule.PLeqTRUE.asl}
@@ -3625,10 +4087,11 @@ \section{SemanticsRule.PLeq \label{sec:SemanticsRule.PLeq}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexprsef{\env, \ve} \evalarrow \Normal(\vv', \vg) \terminateas \ErrorConfig
+    \evalexprsef{\env, \ve} \evalarrow \Normal(\vvone, \newg) \terminateas \ErrorConfig\\
+    \binop(\LEQ, \vv, \vvone) \evalarrow \vb
   }
   {
-    \evalpattern{\env, \vv, \texttt{Pattern\_Geq}(\ve)} \evalarrow \Normal(\binop(\LEQ, \vv, \vv'), \vg)
+    \evalpattern{\env, \vv, \texttt{Pattern\_Leq}(\ve)} \evalarrow \Normal(\vb, \newg)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3636,16 +4099,15 @@ \section{SemanticsRule.PLeq \label{sec:SemanticsRule.PLeq}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.PNot \label{sec:SemanticsRule.PNot}}
-
     \subsection{Prose}
-    Evaluation of the pattern $\vp$ under environment $\env$ with
-    respect to value $\vv$ is \texttt{b} and all of the following apply:
-    \begin{itemize}
-      \item $\vp$ is the negation of the pattern \texttt{p'};
-      \item \texttt{b'} is the result of the evaluation of the pattern
-        \texttt{p'} under environment $\env$ with respect to the value
-        $\vv$;
-      \item \texttt{b} is the boolean negation of \texttt{b'}.
+    evaluation of the pattern $\vp$ under environment $\env$ with
+    respect to value $\vv$ is either $\Normal(\vb, \newg)$ or an error configuration,
+    and all of the following apply:
+      \begin{itemize}
+      \item $\vp$ is the negation of the pattern $\vpone$, that is $\texttt{Pattern\_Not}(\vpone)$;
+      \item evaluating tha pattern $\vpone$ under environment $\env$ is either \\
+      $\Normal(\vbone, \newg)$ \ProseOrError;
+      \item $\vb$ is the Boolean negation of $\vbone$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.PNotTRUE.asl}
@@ -3661,11 +4123,11 @@ \section{SemanticsRule.PNot \label{sec:SemanticsRule.PNot}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexprsef{\env, \ve} \evalarrow \Normal(\vb, \vg) \terminateas \ErrorConfig\\
-    \unop(\BNOT, \vb) \evalarrow \vb'
+    \evalexprsef{\env, \vpone} \evalarrow \Normal(\vbone, \newg) \terminateas \ErrorConfig\\
+    \unop(\BNOT, \vbone) \evalarrow \vb
   }
   {
-    \evalpattern{\env, \vv, \texttt{Pattern\_Not}(\vp')} \evalarrow \Normal(\vb', \vg)
+    \evalpattern{\env, \vv, \texttt{Pattern\_Not}(\vpone)} \evalarrow \Normal(\vb, \newg)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3673,24 +4135,23 @@ \section{SemanticsRule.PNot \label{sec:SemanticsRule.PNot}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.PRange \label{sec:SemanticsRule.PRange}}
-
     \subsection{Prose}
-  Evaluation of the pattern $\vp$ under environment $\env$ with
-  respect to value $\vv$ is \texttt{b} and all of the following apply:
+    evaluation of the pattern $\vp$ under environment $\env$ with
+    respect to value $\vv$ is either $\Normal(\vb, \newg)$ or an error configuration,
+    and all of the following apply:
     \begin{itemize}
       \item $\vp$ is the condition corresponding to being greater or equal
-        to \texttt{e1}, and lesser or equal to \texttt{e2};
-      \item \texttt{e1} and \texttt{e2} are side-effect-free expressions;
-      \item \texttt{v1} is the side-effect-free evaluation of \texttt{e1} in
-        $\env$;
-      \item \texttt{v2} is the side-effect-free evaluation of \texttt{e2} in
-        $\env$;
-      \item \texttt{b1} is the boolean value corresponding to whether
-        $\vv$ is greater or equal to \texttt{v1}.
-      \item \texttt{b2} is the boolean value corresponding to whether
-        $\vv$ is less or equal to \texttt{v2}.
-      \item \texttt{b} is the boolean conjunction of \texttt{b1} and
-        \texttt{b2}.
+        to $\veone$, and lesser or equal to $\vetwo$, that is $\texttt{Pattern\_Range}(\veone, \vetwo)$;
+      \item $\veone$ and $\vetwo$ are side-effect-free expressions;
+      \item the side-effect-free evaluation of $\veone$ in $\env$ is either $\Normal(\vvone, \vgone)$ \ProseOrError;
+      \item the side-effect-free evaluation of $\vetwo$ in $\env$ is either $\Normal(\vvtwo, \vgtwo)$ \ProseOrError;
+      \item $\vbone$ is the Boolean value corresponding to whether
+        $\vv$ is greater or equal to $\vvone$;
+        \item $\vbtwo$ is the Boolean value corresponding to whether
+        $\vv$ is greater or equal to $\vvtwo$;
+      \item $\vb$ is the Boolean conjunction of $\vbone$ and
+      $\vbtwo$;
+      \item $\newg$ is the parallel composition of $\vgone$ and $\vgtwo$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.PRangeTRUE.asl}
@@ -3711,10 +4172,10 @@ \section{SemanticsRule.PRange \label{sec:SemanticsRule.PRange}}
     \evalexprsef{\env, \veone} \evalarrow \Normal(\vvtwo, \vgtwo) \terminateas \ErrorConfig\\
     \binop(\GEQ, \vv, \vvtwo) \evalarrow \vbtwo\\
     \binop(\BAND, \vbone, \vbtwo) \evalarrow \vb\\
-    \vg = \vgone \parallel \vgtwo
+    \newg = \vgone \parallel \vgtwo
   }
   {
-    \evalpattern{\env, \vv, \texttt{Pattern\_Range}(\veone, \vetwo)} \evalarrow \Normal(\vb, \vg)
+    \evalpattern{\env, \vv, \texttt{Pattern\_Range}(\veone, \vetwo)} \evalarrow \Normal(\vb, \newg)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3722,17 +4183,17 @@ \section{SemanticsRule.PRange \label{sec:SemanticsRule.PRange}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.PSingle \label{sec:SemanticsRule.PSingle}}
-
     \subsection{Prose}
-  Evaluation of the pattern $\vp$ under environment $\env$ with
-  respect to value $\vv$ is \texttt{b} and all of the following apply:
+    evaluation of the pattern $\vp$ under environment $\env$ with
+    respect to value $\vv$ is either $\Normal(\vb, \newg)$ or an error configuration,
+    and all of the following apply:
     \begin{itemize}
       \item $\vp$ is the condition corresponding to being equal to the
-        side-effect-free expression $\ve$;
-      \item \texttt{v'} is the side-effect-free evaluation of $\ve$ in
-        environment $\env$;
-      \item \texttt{b} is the boolean value corresponding to whether $\vv$
-        is equal to \texttt{v'}.
+        side-effect-free expression $\ve$, that is $\texttt{Pattern\_Single}(\ve)$;
+      \item the side-effect-free evaluation of $\ve$ in
+        environment $\env$ is either \\ $\Normal(\vvone, \newg)$ \ProseOrError;
+      \item $\vb$ is the boolean value corresponding to whether $\vv$
+        is equal to $\vvone$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.PSingleTRUE.asl}
@@ -3748,11 +4209,11 @@ \section{SemanticsRule.PSingle \label{sec:SemanticsRule.PSingle}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evalexprsef{\env, \veone} \evalarrow \Normal(\vvp, \vg) \terminateas \ErrorConfig\\
-    \binop(\EQOP, \vv, \vvp) \evalarrow \vb
+    \evalexprsef{\env, \veone} \evalarrow \Normal(\vvone, \newg) \terminateas \ErrorConfig\\
+    \binop(\EQOP, \vvone, \vvone) \evalarrow \vb
   }
   {
-    \evalpattern{\env, \vv, \texttt{Pattern\_Single}(\ve)} \evalarrow \Normal(\vb, \vg)
+    \evalpattern{\env, \vv, \texttt{Pattern\_Single}(\ve)} \evalarrow \Normal(\vb, \newg)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3760,12 +4221,13 @@ \section{SemanticsRule.PSingle \label{sec:SemanticsRule.PSingle}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.PMask \label{sec:SemanticsRule.PMask}}
-
     \subsection{Prose}
-    Evaluation of the pattern $\vp$ under environment $\env$ with
-    respect to value $\vv$ is \texttt{b} and all of the following apply:
+    evaluation of the pattern $\vp$ under environment $\env$ with
+    respect to value $\vv$ is either $\Normal(\vb, \newg)$ or an error configuration,
+    and all of the following apply:
     \begin{itemize}
-      \item $\vp$ is a mask \texttt{m} of length $n$ (with spaces removed);
+      \item $\vp$ is a mask $\vm$, that is $\texttt{Pattern\_Mask}(\vm)$,
+      of length $n$ (with spaces removed);
       \item \texttt{m\_set} is the bitvector value of length $n$ with bit set
         at index $i$ if the mask requires a bit set at index $i$, i.\,e.\
         $\texttt{m}[i] = '1'$;
@@ -3798,7 +4260,7 @@ \section{SemanticsRule.PMask \label{sec:SemanticsRule.PMask}}
   \subsection{Formally}
   \newcommand\maskmatch[0]{\text{mask\_match}}
   The helper function $\maskmatch : \{0, 1, \vx\} \times \{0,1\} \rightarrow \{\True,\False\}$,
-  which checks whether a bit value (second operand) matches a mask value (first operand),
+  checks whether a bit value (second operand) matches a mask value (first operand),
   is defined by the following table:
 \[
   \begin{array}{|c|c|c|c|}
@@ -3814,12 +4276,12 @@ \section{SemanticsRule.PMask \label{sec:SemanticsRule.PMask}}
 
 \begin{mathpar}
   \inferrule{
-    \vm \eqname \vm_{1..k}\\
-    \vv \eqname \vv_{1..k}\\
-    \vv = \nvbool(\bigwedge_{i=1..k} \maskmatch(\vm_i, \vv_i))
+    \vm \eqname \vm_{1..n}\\
+    \vv \eqname \vv_{1..n}\\
+    \vb = \nvbool(\bigwedge_{i=1..n} \maskmatch(\vm_i, \vv_i))
   }
   {
-    \evalpattern{\env, \vv, \texttt{Pattern\_Mask}(\vm)} \evalarrow \Normal(\vv, \emptygraph)
+    \evalpattern{\env, \vv, \texttt{Pattern\_Mask}(\vm)} \evalarrow \Normal(\vb, \emptygraph)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3872,26 +4334,32 @@ \section{SemanticsRule.PTuple \label{sec:SemanticsRule.PTuple}}
 \chapter{Evaluation of Local Declarations \label{chap:eval_local_decl}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\texttt{eval\_local\_decl ldi env m\_init\_opt} declares local variables
-\texttt{ldi} in $\env$ with an optional initialisation value
-\texttt{m\_init\_opt}.  Evaluation of the local variables \texttt{ldi}
-under an environment $\env$ is either $\newenv$ or returns an
-error and one of the following applies:
+The relation
+\[
+  \evallocaldecl{\overname{\envs}{\env} \times \localdeclitem \times \langle\overname{\vals}{\vv}\times\overname{\XGraphs}{\vgone}\rangle} \;\aslrel\;
+                         \Normal(\overname{\XGraphs}{\newg}, \overname{\envs}{\newenv})
+\]
+declares local variables
+$\ldi$ in $\env$ with an optional initialisation value
+$\minitopt$.  Evaluation of the local variables $\ldi$
+under an environment $\env$ is either $\Normal(\vg, \newenv)$
+or an abnormal configuration and one of the following applies:
 \begin{itemize}
-  \item SemanticsRule.LDDiscard (see Section~\ref{sec:SemanticsRule.LDDiscard}),
-  \item SemanticsRule.LDVar (see Section~\ref{sec:SemanticsRule.LDVar}),
-  \item SemanticsRule.LDTyped (see Section~\ref{sec:SemanticsRule.LDTyped}),
-  \item SemanticsRule.LDTuple (see Section~\ref{sec:SemanticsRule.LDTuple}),
-  \item SemanticsRule.LDUninitialisedTyped (see Section~\ref{sec:SemanticsRule.LDUninitialisedTyped}),
+  \item SemanticsRule.LDDiscard (see \secref{SemanticsRule.LDDiscard}),
+  \item SemanticsRule.LDVar (see \secref{SemanticsRule.LDVar}),
+  \item SemanticsRule.LDTyped (see \secref{SemanticsRule.LDTyped}),
+  \item SemanticsRule.LDTuple (see \secref{SemanticsRule.LDTuple}),
+  \item SemanticsRule.LDUninitialisedTyped (see \secref{SemanticsRule.LDUninitialisedTyped}),
 \end{itemize}
 
 \section{SemanticsRule.LDDiscard \label{sec:SemanticsRule.LDDiscard}}
-
     \subsection{Prose}
-Evaluation of the local variables \texttt{ldi} under the environment
-$\env$ is $\newenv$ and all of the following apply:
+    Evaluation of the local variables $\ldi$ under the environment \\
+    $\env$ is $\Normal(\vg, \newenv)$ and all of the following apply:
     \begin{itemize}
-    \item \texttt{ldi} indicates that the initialisation value will be discarded;
+    \item $\ldi$ indicates that the initialisation value will be discarded,
+    that is \\ $\texttt{LDI\_Discard}$;
+    \item $\newg$ is the empty graph;
     \item $\newenv$ is $\env$.
     \end{itemize}
 
@@ -3916,15 +4384,15 @@ \section{SemanticsRule.LDDiscard \label{sec:SemanticsRule.LDDiscard}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.LDVar \label{sec:SemanticsRule.LDVar}}
-
     \subsection{Prose}
-Evaluation of the local variables \texttt{ldi} under the environment
-$\env$ is $\newenv$ and all of the following apply:
+    Evaluation of the local variables $\ldi$ under the environment \\
+    $\env$ is $\Normal(\vg, \newenv)$ and all of the following apply:
     \begin{itemize}
-    \item \texttt{ldi} is a variable \vx;
-    \item \texttt{m\_init\_opt} is a value \texttt{m};
-    \item $\newenv$ is $\env$ modified to declare \texttt{x} as a
-local variable bound to value \texttt{m}.
+    \item $\ldi$ is a variable \vx, that is $\texttt{LDI\_Var}(\vx)$;
+    \item $\minitopt$ is $\vm$;
+    \item $\vm$ is a pair consisting of the value $\vv$ and execution graph $\vgone$;
+    \item declaring $\vx$ in $\env$ is $(\newenv, \vgtwo)$;
+    \item $\newg$ is the ordered composition of $\vgone$ and $\vgtwo$ with the data label.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.LDVar0.asl}
@@ -3947,10 +4415,10 @@ \section{SemanticsRule.LDVar \label{sec:SemanticsRule.LDVar}}
   \inferrule{
     \vm \eqname (\vv, \vgone)\\
     \declarelocalidentifier(\env, \vx, \vv)\evalarrow(\newenv, \vgtwo)\\
-    \vg = \ordered{\vgone}{\asldata}{\vgtwo}
+    \newg = \ordered{\vgone}{\asldata}{\vgtwo}
   }
   {
-    \evallocaldecl{\env, \texttt{LDI\_Var}(\vx), \langle \vm\rangle} \evalarrow \Normal(\vg, \newenv)
+    \evallocaldecl{\env, \texttt{LDI\_Var}(\vx), \langle \vm\rangle} \evalarrow \Normal(\newg, \newenv)
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3960,17 +4428,16 @@ \section{SemanticsRule.LDVar \label{sec:SemanticsRule.LDVar}}
 \section{SemanticsRule.LDTyped \label{sec:SemanticsRule.LDTyped}}
 
     \subsection{Prose}
-Evaluation of the local variables \texttt{ldi} under the environment
-$\env$ is $\newenv$ and all of the following apply:
+    Evaluation of the local variables $\ldi$ under the environment \\
+    $\env$ is $\Normal(\vg, \newenv)$ or an abnormal configuration
+    and all of the following apply:
     \begin{itemize}
-      \item \texttt{ldi} gives a local declaration item \texttt{ldi'} and a
-        type \texttt{t};
-        %
-      \item \texttt{m\_init\_opt} is a value \texttt{m};
-        %
-      \item $\newenv$ is $\env$ modified after the evaluation of
-        \texttt{ldi'} with the initialisation value \texttt{m} in $\env$.
-        %
+      \item $\ldi$ gives a local declaration item $\ldione$ and a
+        type $\vt$, that is \\ $\texttt{LDI\_Typed}(\ldione, \vt)$;
+      \item $\minitopt$ is $\vm$;
+      \item the resulting configuration is obtained via the evaluation
+      of the local declaration $\ldione$ under $\env$ with $\minitopt$ as $\vm$,
+      that is \\ $\evallocaldecl{\env, \ldi1, \langle \vm\rangle}$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.LDTyped.asl}
@@ -3985,10 +4452,10 @@ \section{SemanticsRule.LDTyped \label{sec:SemanticsRule.LDTyped}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \evallocaldecl{\env, \ldi', \langle \vm\rangle} \evalarrow C
+    \evallocaldecl{\env, \ldi1, \langle \vm\rangle} \evalarrow C
   }
   {
-    \evallocaldecl{\env, \texttt{LDI\_Typed}(\ldi', \Ignore), \langle \vm\rangle} \evalarrow C
+    \evallocaldecl{\env, \texttt{LDI\_Typed}(\ldi1, \Ignore), \langle \vm\rangle} \evalarrow C
   }
 \end{mathpar}
 \end{emptyformal}
@@ -3996,15 +4463,20 @@ \section{SemanticsRule.LDTyped \label{sec:SemanticsRule.LDTyped}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.LDTuple \label{sec:SemanticsRule.LDTuple}}
-
     \subsection{Prose}
-Evaluation of the local variables \texttt{ldi} under the environment
-$\env$ is $\newenv$ and all of the following apply:
+    Evaluation of the local variables $\ldi$ under the environment \\
+    $\env$ is $\Normal(\vg, \newenv)$ or an abnormal configuration
+    and all of the following apply:
     \begin{itemize}
-    \item \texttt{ldi} gives a list of local variables \texttt{ldis};
-    \item \texttt{m\_init\_opt} is a list of values \texttt{liv};
-    \item $\newenv$ is $\env$ modified to declare each element of \texttt{ldis} to be bound
-      to the corresponding value in \texttt{liv}.
+    \item $\ldi$ gives a list of local variables $\ldis$, that is \\
+    $\texttt{LDI\_Tuple}(\ldis)$;
+    \item $\minitopt$ is $\vm$;
+    \item $\vm$ is a pair consisting of the native vector $\vv$ and execution graph $\vg$;
+    \item $\ldis$ is a list of local declaration items $\ldi_{1..k}$;
+    \item the value at each index of $\vv$ is $\vv_i$, for $i=1..k$;
+    \item $\liv$ is the list of pairs $(\vv_i, \vg)$, for $i=1..k$;
+    \item the output configuration is obtained by declare each local declaration item $\ldi_i$
+    with the corresponding value ($\minitopt$ component) $(\vv_i, \vg)$.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.LDTuple.asl}
@@ -4039,10 +4511,10 @@ \section{SemanticsRule.LDTuple \label{sec:SemanticsRule.LDTuple}}
     \vm \eqname (\vv, \vgone)\\
     \evallocaldecl{\env, \ldi, \langle\vm\rangle} \evalarrow \Normal(\vgone, \envone)\\
     \ldituplefolder{\envone, \ldis', \liv'} \evalarrow \Normal(\vgtwo, \newenv)\\
-    \vg = \vgone \parallel \vgtwo
+    \newg = \vgone \parallel \vgtwo
   }
   {
-    \ldituplefolder{\env, \ldis, \liv} \evalarrow \Normal(\vg, \newenv)
+    \ldituplefolder{\env, \ldis, \liv} \evalarrow \Normal(\newg, \newenv)
   }
 \end{mathpar}
 
@@ -4064,21 +4536,17 @@ \section{SemanticsRule.LDTuple \label{sec:SemanticsRule.LDTuple}}
 \isempty{\subsection{Comments}}
 
 \section{SemanticsRule.LDUninitialisedTyped\label{sec:SemanticsRule.LDUninitialisedTyped}}
-
     \subsection{Prose}
-    Evaluation of the local declaration item \texttt{ldi} under the environment
-    $\env$ is $\newenv$ and all of the following apply:
+    Evaluation of the local variables $\ldi$ under the environment \\
+    $\env$ is $\Normal(\vg, \newenv)$ or an abnormal configuration
+    and all of the following apply:
     \begin{itemize}
-      \item \texttt{ldi} gives a local declaration item \texttt{ldi'} and a
-        type \texttt{t};
-        %
-      \item \texttt{m\_init\_opt} is \texttt{None};
-        %
-      \item \texttt{m} is the base value of \texttt{t} in $\env$;
-        %
-      \item $\newenv$ is $\env$ modified after the evaluation of
-        \texttt{ldi'} with the initialisation value \texttt{m} in $\env$.
-        %
+      \item $\ldi$ gives a local declaration item $\ldione$ and a
+        type $\vt$, that is, \\ $\texttt{LDI\_Ttyped}(\ldione, \vt)$;
+      \item $\minitopt$ is $\None$;
+      \item the base value of $\vt$ is either $\vm$ \ProseOrError;
+      \item evaluating the local declaration $\ldione$ with $\vm$
+      as the $\minitopt$ component yields the output configuration.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.LDUninitialisedTyped.asl}
@@ -4094,10 +4562,10 @@ \section{SemanticsRule.LDUninitialisedTyped\label{sec:SemanticsRule.LDUninitiali
 \begin{mathpar}
   \inferrule{
     \basevalue(\env, \vt) \evalarrow \vm \terminateas \ErrorConfig\\
-    \evallocaldecl{\env, \ldi', \langle \vm \rangle} \evalarrow C
+    \evallocaldecl{\env, \ldione, \langle \vm \rangle} \evalarrow C
   }
   {
-    \evallocaldecl{\env, \texttt{LDI\_Ttyped}(\ldi', \vt), \None} \evalarrow C
+    \evallocaldecl{\env, \texttt{LDI\_Ttyped}(\ldione, \vt), \None} \evalarrow C
   }
 \end{mathpar}
 \end{emptyformal}
@@ -4110,7 +4578,7 @@ \chapter{Evaluation of Statements \label{chap:eval_stmt}}
 
 The semantic relation for statements is defined as follows:
 \[
-  \semantic{\texttt{stmt}} : \evalstmt{\envs \times \stmt} \times \left(
+  \evalstmt{\envs \times \stmt} \times \left(
     \begin{array}{ll}
     \Continuing(\XGraphs, \envs) &\cup\\
     \Returning((\vals^* \times \XGraphs), \envs) &\cup\\
@@ -4128,26 +4596,26 @@ \chapter{Evaluation of Statements \label{chap:eval_stmt}}
 or with a given exception value and an associated exception type.
 
 \begin{itemize}
-\item SemanticsRule.SPass (see Section~\ref{sec:SemanticsRule.SPass}),
-\item SemanticsRule.SAssign (see Section~\ref{sec:SemanticsRule.SAssign}),
-\item SemanticsRule.SAssignCall (see Section~\ref{sec:SemanticsRule.SAssignCall}),
-\item SemanticsRule.SAssignTuple (see Section~\ref{sec:SemanticsRule.SAssignTuple}),
-\item SemanticsRule.SReturnNone (see Section~\ref{sec:SemanticsRule.SReturnNone}),
-\item SemanticsRule.SReturnOne (see Section~\ref{sec:SemanticsRule.SReturnOne}),
-\item SemanticsRule.SReturnSome (see Section~\ref{sec:SemanticsRule.SReturnSome}),
-\item SemanticsRule.SSeq (see Section~\ref{sec:SemanticsRule.SSeq}),
-\item SemanticsRule.SCall (see Section~\ref{sec:SemanticsRule.SCall}),
-\item SemanticsRule.SCond (see Section~\ref{sec:SemanticsRule.SCond}),
-\item SemanticsRule.SCase (see Section~\ref{sec:SemanticsRule.SCase}),
-\item SemanticsRule.SAssert (see Section~\ref{sec:SemanticsRule.SAssert}),
-\item SemanticsRule.SWhile (see Section~\ref{sec:SemanticsRule.SWhile}),
-\item SemanticsRule.SRepeat (see Section~\ref{sec:SemanticsRule.SRepeat}),
-\item SemanticsRule.SFor (see Section~\ref{sec:SemanticsRule.SFor}),
-\item SemanticsRule.SThrowNone (see Section~\ref{sec:SemanticsRule.SThrowNone}),
-\item SemanticsRule.SThrowSomeTyped (see Section~\ref{sec:SemanticsRule.SThrowSomeTyped}),
-\item SemanticsRule.STry (see Section~\ref{sec:SemanticsRule.STry}),
-\item SemanticsRule.SDeclSome (see Section~\ref{sec:SemanticsRule.SDeclSome}),
-\item SemanticsRule.SDeclNone (see Section~\ref{sec:SemanticsRule.SDeclNone}).
+\item SemanticsRule.SPass (see \secref{SemanticsRule.SPass}),
+\item SemanticsRule.SAssign (see \secref{SemanticsRule.SAssign}),
+\item SemanticsRule.SAssignCall (see \secref{SemanticsRule.SAssignCall}),
+\item SemanticsRule.SAssignTuple (see \secref{SemanticsRule.SAssignTuple}),
+\item SemanticsRule.SReturnNone (see \secref{SemanticsRule.SReturnNone}),
+\item SemanticsRule.SReturnOne (see \secref{SemanticsRule.SReturnOne}),
+\item SemanticsRule.SReturnSome (see \secref{SemanticsRule.SReturnSome}),
+\item SemanticsRule.SSeq (see \secref{SemanticsRule.SSeq}),
+\item SemanticsRule.SCall (see \secref{SemanticsRule.SCall}),
+\item SemanticsRule.SCond (see \secref{SemanticsRule.SCond}),
+\item SemanticsRule.SCase (see \secref{SemanticsRule.SCase}),
+\item SemanticsRule.SAssert (see \secref{SemanticsRule.SAssert}),
+\item SemanticsRule.SWhile (see \secref{SemanticsRule.SWhile}),
+\item SemanticsRule.SRepeat (see \secref{SemanticsRule.SRepeat}),
+\item SemanticsRule.SFor (see \secref{SemanticsRule.SFor}),
+\item SemanticsRule.SThrowNone (see \secref{SemanticsRule.SThrowNone}),
+\item SemanticsRule.SThrowSomeTyped (see \secref{SemanticsRule.SThrowSomeTyped}),
+\item SemanticsRule.STry (see \secref{SemanticsRule.STry}),
+\item SemanticsRule.SDeclSome (see \secref{SemanticsRule.SDeclSome}),
+\item SemanticsRule.SDeclNone (see \secref{SemanticsRule.SDeclNone}).
 \end{itemize}
 
 \section{SemanticsRule.SPass \label{sec:SemanticsRule.SPass}}
@@ -4187,7 +4655,7 @@ \section{SemanticsRule.SAssign \label{sec:SemanticsRule.SAssign}}
   \item \texttt{s} is an assignment \texttt{le = re};
   \item $\vv$ is the evaluation of the expression \texttt{re} under $\env$ as per Chapter~\ref{chap:eval_expr};
   \item \texttt{r\_env} is $\env$ modified after evaluation of the expression \texttt{re} under $\env$ as per Chapter~\ref{chap:eval_expr};
-  \item $\newenv$ is \texttt{r\_env} modified after evaluation of \texttt{le} under \texttt{r\_env} with
+  \item $\newenv$ is \texttt{r\_env} modified after evaluation of $\vle$ under \texttt{r\_env} with
     $\vv$, as per Chapter~\ref{chap:eval_lexpr}.
   \end{itemize}
 
@@ -4582,17 +5050,52 @@ \section{SemanticsRule.SCase \label{sec:SemanticsRule.SCase}}
 
 \begin{emptyformal}
   \subsection{Formally}
-A case statement is syntactic sugar for a ``condition-ladder''.
-We use the AST-to-AST function \tododefine{case\_to\_conds} to convert a case statement
-into a corresponding conditional statement.
+  \newcommand\casetoconds[0]{\texttt{case\_to\_conds}}
+  \newcommand\caselist[0]{\texttt{case\_list}}
+  \newcommand\casecond[0]{\texttt{case\_cond}}
+A case statement is syntactic sugar for a ``condition ladder'' where each
+of the alternatives is a pattern.
+We define the relation
+\[
+  \casetoconds(\expr, (\pattern \times \stmt)^*) \;\bigtimes\; \stmt
+\]
+which performs this AST-to-AST transformation, effectively desugaring
+the case statement.
+
+\begin{mathpar}
+  \inferrule{}
+  {
+    \casetoconds(\texttt{E\_Var}(\vx), \emptylist) \evalarrow \texttt{S\_Pass}
+  }
+  \and
+  \inferrule{
+    \casetoconds(\texttt{E\_Var}(\vx), \caselist) \evalarrow \caselist'
+  }
+  {
+    \casetoconds(\texttt{E\_Var}(\vx), [(\vp, \vs)] + \caselist) \evalarrow \\
+    \texttt{S\_Cond}(\texttt{E\_Pattern}(\texttt{E\_Var}(\vx), \vp), \vs, \caselist')
+  }
+  \and
+  \inferrule{
+    \ve \not\in \{\texttt{E\_Var}(\vx) \;|\; \vx \in \identifier\}\\
+    \vy \in \identifier \text{ is fresh}\\
+    \texttt{var\_decl} = \texttt{S\_Decl}(\texttt{LDK\_Let}, \texttt{LDI\_Typed}(\texttt{LDI\_Var}(\vy), \texttt{T\_Int}(\texttt{UnConstrained})))\\
+    \casetoconds(\texttt{E\_Var}(\vy), \caselist) \evalarrow \casecond
+  }
+  {
+    \casetoconds(\ve, \caselist) \evalarrow
+    \texttt{S\_Seq}(\texttt{var\_decl}, \casecond)
+  }
+\end{mathpar}
 
+We now define the semantics of a case statement in terms of the desugared statement:
 \begin{mathpar}
   \inferrule{
-    \tododefine{case\_to\_conds}(\ve, \texttt{alts}) = \vs\\
+    \casetoconds(\ve, \caselist) \evalarrow \vs\\
     \evalstmt{\env, \vs} \evalarrow C
   }
   {
-    \evalstmt{\env, \texttt{S\_Case}(\ve, \texttt{alts})} \evalarrow C
+    \evalstmt{\env, \texttt{S\_Case}(\ve, \caselist)} \evalarrow C
   }
 \end{mathpar}
 \end{emptyformal}
@@ -4604,7 +5107,7 @@ \section{SemanticsRule.SAssert \label{sec:SemanticsRule.SAssert}}
     \subsection{Prose}
   Evaluation of the statement \texttt{s} under environment $\env$ is
 $\newenv$ or an error and all of the following apply:
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s} is an \texttt{assert} statement;
     \item \texttt{s} gives an expression $\ve$;
@@ -4645,7 +5148,7 @@ \section{SemanticsRule.SAssert \label{sec:SemanticsRule.SAssert}}
     \vv = \nvbool(\False)
   }
   {
-    \evalstmt{\env, \texttt{S\_Assert}(\ve)} \evalarrow \Error(\texttt{"Assertion failed!"})
+    \evalstmt{\env, \texttt{S\_Assert}(\ve)} \evalarrow \ErrorVal{AssertionFailed}
   }
 \end{mathpar}
 \end{emptyformal}
@@ -4660,7 +5163,7 @@ \section{SemanticsRule.SWhile \label{sec:SemanticsRule.SWhile}}
     \begin{itemize}
     \item \texttt{s} is a \texttt{while} statement;
     \item \texttt{s} gives an expression $\ve$ and a loop body \texttt{body};
-    \item $\newenv$ is $\env$ modified after evaluation of the loop \texttt{(e,body)} as per Section~\ref{sec:SemanticsRule.Loop}.
+    \item $\newenv$ is $\env$ modified after evaluation of the loop \texttt{(e,body)} as per \secref{SemanticsRule.Loop}.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.SWhile.asl}
@@ -4693,7 +5196,7 @@ \section{SemanticsRule.SRepeat \label{sec:SemanticsRule.SRepeat}}
     \begin{itemize}
     \item \texttt{s} is a \texttt{repeat} statement;
     \item \texttt{s} gives an expression $\ve$ and a loop body \texttt{body};
-    \item $\newenv$ is $\env$ modified after evaluation of the loop \texttt{(e,body)} as per Section~\ref{sec:SemanticsRule.Loop}.
+    \item $\newenv$ is $\env$ modified after evaluation of the loop \texttt{(e,body)} as per \secref{SemanticsRule.Loop}.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.SRepeat.asl}
@@ -4727,7 +5230,7 @@ \section{SemanticsRule.SFor \label{sec:SemanticsRule.SFor}}
     \begin{itemize}
     \item \texttt{s} is a \texttt{for} statement;
     \item \texttt{s} gives \texttt{(id,e1,dir,e2,s)};
-    \item $\newenv$ is $\env$ modified after evaluation of the \texttt{for} loop \texttt{(id,e1,dir,e2,s)} as per Section~\ref{sec:SemanticsRule.For}.
+    \item $\newenv$ is $\env$ modified after evaluation of the \texttt{for} loop \texttt{(id,e1,dir,e2,s)} as per \secref{SemanticsRule.For}.
     \end{itemize}
 
     \subsection{Example: SemanticsRule.SFor.asl}
@@ -4763,7 +5266,7 @@ \section{SemanticsRule.SFor \label{sec:SemanticsRule.SFor}}
 \section{SemanticsRule.SThrowNone \label{sec:SemanticsRule.SThrowNone}}
 
     \subsection{Prose}
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s} is a \texttt{throw} statement which gives no expression;
     \item $\newenv$ is $\env$;
@@ -4793,7 +5296,7 @@ \section{SemanticsRule.SThrowNone \label{sec:SemanticsRule.SThrowNone}}
 \section{SemanticsRule.SThrowSomeTyped \label{sec:SemanticsRule.SThrowSomeTyped}}
 
     \subsection{Prose}
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s} is a \texttt{throw} statement which gives an expression $\ve$ and a type \texttt{t};
     \item $\vv$ is the result of evaluating the expression $\ve$ in $\env$;
@@ -4816,10 +5319,10 @@ \subsection{Formally}
     \evalexpr{\env, \ve} \evalarrow \Normal((\vv, \vgone), \newenv) \OrAbnormal\\
     \vgtwo = \WriteEffect(\name)\\
     \name\in\identifier \text{ is fresh}\\
-    \vg' = \ordered{\vgone}{\asldata}{\vgtwo}
+    \newg = \ordered{\vgone}{\asldata}{\vgtwo}
   }
   {
-    \evalstmt{\env, \texttt{S\_Throw}(\langle\ve, \langle\vt\rangle\rangle)} \evalarrow \Throwing((\langle(\vv,\vt)\rangle, \vg'), \env)
+    \evalstmt{\env, \texttt{S\_Throw}(\langle\ve, \langle\vt\rangle\rangle)} \evalarrow \Throwing((\langle((\vv, \name),\vt)\rangle, \newg), \env)
   }
   \end{mathpar}
 \end{emptyformal}
@@ -5003,11 +5506,11 @@ \chapter{Evaluation of Loops \label{chap:eval_loops}}
 statements.
 %
 For example, the semantic rule \emph{Loop} is used by the semantic rule
-\emph{SWhile} at Section~\ref{sec:SemanticsRule.SWhile} and the semantic rule
-\emph{SRepeat} at Section~\ref{sec:SemanticsRule.SRepeat}.
+\emph{SWhile} at \secref{SemanticsRule.SWhile} and the semantic rule
+\emph{SRepeat} at \secref{SemanticsRule.SRepeat}.
 %
 The semantic rule \emph{For} is only used by the semantic rule \emph{SFor} at
-Section~\ref{sec:SemanticsRule.SFor}.
+\secref{SemanticsRule.SFor}.
 
 \section{SemanticsRule.Loop \label{sec:SemanticsRule.Loop}}
 \texttt{eval\_loop is\_while env e\_cond body} evaluates \texttt{body} in
@@ -5018,12 +5521,12 @@ \section{SemanticsRule.Loop \label{sec:SemanticsRule.Loop}}
     \texttt{cond\_m} evaluates to \texttt{e\_cond} or \texttt{not e\_cond} as
 determined by \texttt{is\_while} and one of the following applies:
     \begin{itemize}
-    \item All of the following apply:
+    \item all of the following apply:
       \begin{itemize}
       \item \texttt{cond\_m} evaluates to \texttt{false};
       \item $\newenv$ is $\env$---the loop is exited.
       \end{itemize}
-    \item All of the following apply:
+    \item all of the following apply:
       \begin{itemize}
       \item \texttt{cond\_m} evaluates to \texttt{true};
       \item \texttt{env1} is $\env$ modified after the evaluation of the
@@ -5079,12 +5582,12 @@ \section{SemanticsRule.For \label{sec:SemanticsRule.For}}
 v\_end v\_start} as determined by \texttt{dir} and one of the following
 applies:
     \begin{itemize}
-    \item All of the following apply:
+    \item all of the following apply:
       \begin{itemize}
       \item \texttt{cond\_m} evaluates to \texttt{true};
       \item $\newenv$ is $\env$ as the loop is exited.
       \end{itemize}
-    \item All of the following apply:
+    \item all of the following apply:
       \begin{itemize}
       \item \texttt{cond\_m} evaluates to \texttt{false};
       \item \texttt{env1} is $\env$ modified after the evaluation of the statement \texttt{body};
@@ -5206,11 +5709,11 @@ \chapter{Evaluation of Catchers \label{chap:eval_catchers}}
 interruption \texttt{Returning vs} or a new environment $\newenv$.
 Formally, one of the following applies:
 \begin{itemize}
-\item SemanticsRule.Catch (see Section~\ref{sec:SemanticsRule.Catch}),
-\item SemanticsRule.CatchNamed (see Section~\ref{sec:SemanticsRule.CatchNamed}),
-\item SemanticsRule.CatchOtherwise (see Section~\ref{sec:SemanticsRule.CatchOtherwise}),
-\item SemanticsRule.CatchNone (see Section~\ref{sec:SemanticsRule.CatchNone}),
-\item SemanticsRule.CatchNoThrow (see Section~\ref{sec:SemanticsRule.CatchNoThrow}).
+\item SemanticsRule.Catch (see \secref{SemanticsRule.Catch}),
+\item SemanticsRule.CatchNamed (see \secref{SemanticsRule.CatchNamed}),
+\item SemanticsRule.CatchOtherwise (see \secref{SemanticsRule.CatchOtherwise}),
+\item SemanticsRule.CatchNone (see \secref{SemanticsRule.CatchNone}),
+\item SemanticsRule.CatchNoThrow (see \secref{SemanticsRule.CatchNoThrow}).
 \end{itemize}
 
 \newcommand\findcatcher[0]{\texttt{find\_catcher}}
@@ -5269,7 +5772,7 @@ \chapter{Evaluation of Catchers \label{chap:eval_catchers}}
 \section{SemanticsRule.Catch \label{sec:SemanticsRule.Catch}}
 
     \subsection{Prose}
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s\_m} is \texttt{Throwing (v, v\_ty, env\_throw)};
     \item \texttt{catcher} is the first catcher in \texttt{catchers} that matches \texttt{v\_ty};
@@ -5321,7 +5824,7 @@ \section{SemanticsRule.Catch \label{sec:SemanticsRule.Catch}}
 \section{SemanticsRule.CatchNamed \label{sec:SemanticsRule.CatchNamed}}
 
     \subsection{Prose}
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s\_m} is \texttt{Throwing (v, v\_ty, env\_throw)};
     \item \texttt{catcher} is the first catcher in \texttt{catchers} that matches \texttt{v\_ty};
@@ -5358,12 +5861,12 @@ \section{SemanticsRule.CatchNamed \label{sec:SemanticsRule.CatchNamed}}
   \subsection{Formally}
 \begin{mathpar}
   \inferrule{
-    \sm \eqname \Throwing((\langle \vv, \vvty \rangle, \sg), \envthrow)\\
+    \sm \eqname \Throwing((\langle \valuereadfrom(\vv, \eid), \vvty \rangle, \sg), \envthrow)\\
     \env \eqname (\tenv, (G^\denv, L^\denv))\\
     \envthrow = (\tenv, (G^{\denvthrow}, L^{\denvthrow}))\\
     \envone = (\tenv, (G^{\denvthrow}, L^{\denv}))\\
     \findcatcher(\tenv, \vvty, \catchers) = \langle (\langle\name\rangle, \Ignore, \vs) \rangle\\
-    \tododefine{read\_value\_from}(\vv) = (\vvone, \vgone)\\
+    \vgone = \readidentifier(\eid, \vv)\\
     \declarelocalidentifierm(\envone, \name, (\veone, \vgone)) \evalarrow (\envtwo, \vgtwo)\\
     \evalblock{\envtwo, \vs} \evalarrow C \terminateas \ErrorConfig\\
     \envthree = \environof{C}\\
@@ -5382,7 +5885,7 @@ \section{SemanticsRule.CatchNamed \label{sec:SemanticsRule.CatchNamed}}
 \section{SemanticsRule.CatchOtherwise \label{sec:SemanticsRule.CatchOtherwise}}
 
     \subsection{Prose}
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s\_m} is \texttt{Throwing (v, v\_ty, env\_throw)};
     \item \texttt{otherwise\_opt} is \texttt{Some s};
@@ -5433,7 +5936,7 @@ \section{SemanticsRule.CatchOtherwise \label{sec:SemanticsRule.CatchOtherwise}}
 \section{SemanticsRule.CatchNone \label{sec:SemanticsRule.CatchNone}}
 
     \subsection{Prose}
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s\_m} is \texttt{Throwing (v, v\_ty, env\_throw)};
     \item \texttt{otherwise\_opt} is \texttt{None};
@@ -5468,7 +5971,7 @@ \subsection{Formally}
 \section{SemanticsRule.CatchNoThrow \label{sec:SemanticsRule.CatchNoThrow}}
 
     \subsection{Prose}
-    All of the following apply:
+    all of the following apply:
     \begin{itemize}
     \item \texttt{s\_m} is not \texttt{Throwing};
     \item $\vres$ is \texttt{s\_m}.
@@ -5544,8 +6047,8 @@ \chapter{Evaluation of Subprograms \label{chap:eval_call}}
 $\newenv$ and a list of values \texttt{vs}, or an error is returned.
 One of the following applies:
 \begin{itemize}
-\item SemanticsRule.FPrimitive (see Section~\ref{sec:SemanticsRule.FPrimitive}),
-\item SemanticsRule.FCall (see Section~\ref{sec:SemanticsRule.FCall}).
+\item SemanticsRule.FPrimitive (see \secref{SemanticsRule.FPrimitive}),
+\item SemanticsRule.FCall (see \secref{SemanticsRule.FCall}).
 \end{itemize}
 
 \section{SemanticsRule.Call \label{sec:SemanticsRule.Call}}
@@ -5585,7 +6088,7 @@ \subsection{Formally}
 \section{SemanticsRule.FPrimitive \label{sec:SemanticsRule.FPrimitive}}
 
   \subsection{Prose}
-  All of the following apply:
+  all of the following apply:
   \begin{itemize}
   \item \texttt{name} is bound in \texttt{genv} to a primitive subprogram with a body \texttt{body};
   \item \texttt{new\_genv} is \texttt{genv};
@@ -5649,7 +6152,7 @@ \section{SemanticsRule.FPrimitive \label{sec:SemanticsRule.FPrimitive}}
 \section{SemanticsRule.FCall \label{sec:SemanticsRule.FCall}}
 
   \subsection{Prose}
-  All of the following apply:
+  all of the following apply:
   \begin{itemize}
   \item \texttt{name} is bound in \texttt{genv} to a subprogram with a list of formal arguments
     \texttt{arg\_decls} and a body statement \texttt{body};
@@ -5799,12 +6302,12 @@ \chapter{Evaluation of Specifications \label{chap:eval_spec}}
   \item One of the following applies:
         \begin{itemize}
 	\item $\vres$ is a value $\vv$, or
-	\item All of the following apply:
+	\item all of the following apply:
               \begin{itemize}
               \item $\vres$ is an implicitly thrown exception;
 	      \item An error ``\texttt{Uncaught exception: implicitly thrown out of a try-catch}'' is returned;
               \end{itemize}
-	\item All of the following apply:
+	\item all of the following apply:
               \begin{itemize}
               \item $\vres$ is an exception \texttt{exn} with an associated type \texttt{ty};
 	      \item An error ``\texttt{Uncaught exception: \{ty\} \{exn\}}'' is returned.
@@ -5914,7 +6417,7 @@ \chapter{Evaluation of Specifications \label{chap:eval_spec}}
     \evalsubprogram{\env, \texttt{"main"}, \emptylist, \emptylist} \evalarrow \Throwing(\texttt{v\_opt}, \Ignore)
   }
   {
-    \evalspec{\parsedspec, \parsedstd} \evalarrow \Error(\texttt{"Uncaught exception!"})
+    \evalspec{\parsedspec, \parsedstd} \evalarrow \ErrorVal{UncaughtException}
   }
 \end{mathpar}
 Notice that when the type-checker fails due to a type error in the given specification,
diff --git a/asllib/doc/ASLSyntaxReference.tex b/asllib/doc/ASLSyntaxReference.tex
index d5b2316579..48daa982f8 100644
--- a/asllib/doc/ASLSyntaxReference.tex
+++ b/asllib/doc/ASLSyntaxReference.tex
@@ -415,5 +415,26 @@ \section{ASL Typed Abstract Syntax}
 This reflects the fact that all other slicing constructs are syntactic sugar
 for \slicelength.
 
+\chapter{Correpondence Betwen Left-hand-side Expressions and Right-hand-side Expressions
+\label{ch:LeftToRight}}
+
+The recursive function $\torexpr : \lexpr \rightarrow \expr$ transforms
+left-hand-side expressions to corresponding right-hand-side expressions,
+which is utilized both for the type system and semantics:
+\[
+\begin{array}{lcl}
+  \textbf{Left hand side expression} & & \textbf{Right hand side expression}\\
+  \hline
+  \torexpr(\texttt{LE\_Var}(\vx)) &=& \texttt{E\_Var}(\vx)\\
+  \torexpr(\leslice(\vle, \vargs)) &=& \texttt{E\_Slice}(\torexpr(\vle), \vargs)\\
+  \torexpr(\texttt{LE\_SetArray}(\vle, \ve)) &=& \texttt{E\_GetArray}(\torexpr(\vle), \ve)\\
+  \torexpr(\texttt{LE\_SetField}(\vle, \vx)) &=& \texttt{E\_GetField}(\torexpr(\vle), \vx)\\
+  \torexpr(\texttt{LE\_SetFields}(\vle, \vx)) &=& \texttt{E\_GetFields}(\torexpr(\vle), \vx)\\
+  \torexpr(\texttt{LE\_Discard}) &=& \texttt{E\_Var("-")}\\
+  \torexpr(\texttt{LE\_Destructuring}([\vle_{1..k}])) &=& \texttt{E\_Tuple}([i=1..k: \torexpr(\vle_i)])\\
+  \torexpr(\texttt{LE\_Concat}([\vle_{1..k}], \Ignore)) &=& \texttt{E\_Concat}([i=1..k: \torexpr(\vle_i)])\\
+\end{array}
+\]
+
 
 \end{document}
diff --git a/asllib/doc/ASLTypingReference.tex b/asllib/doc/ASLTypingReference.tex
index a0cdab31fc..197252aa6f 100644
--- a/asllib/doc/ASLTypingReference.tex
+++ b/asllib/doc/ASLTypingReference.tex
@@ -17,8 +17,6 @@
 
 \newcommand\dynamicdomain[0]{\textsf{dyn-dom}}
 
-\newcommand\astlabel[0]{\textsf{label}}
-
 \newcommand\isbuiltinsingular[0]{\texttt{is\_builtin\_singular}}
 \newcommand\isbuiltinaggregate[0]{\texttt{is\_builtin\_aggregate}}
 \newcommand\isbuiltin[0]{\texttt{is\_builtin}}
@@ -97,17 +95,14 @@
 \newcommand\vl[0]{\texttt{l}}
 \newcommand\vp[0]{\texttt{p}}
 \newcommand\vo[0]{\texttt{o}}
-\newcommand\vx[0]{\texttt{x}}
 \newcommand\vv[0]{\texttt{v}}
 \newcommand\vt[0]{\texttt{t}}
 \newcommand\vte[0]{\texttt{t\_e}}
-\newcommand\ve[0]{\texttt{e}}
 \newcommand\veone[0]{\texttt{e1}}
 \newcommand\vetwo[0]{\texttt{e2}}
 \newcommand\vleone[0]{\texttt{le1}}
 \newcommand\vletwo[0]{\texttt{le2}}
 \newcommand\vtleone[0]{\texttt{t\_le1}}
-\newcommand\vle[0]{\texttt{le}}
 \newcommand\vre[0]{\texttt{re}}
 \newcommand\vs[0]{\texttt{s}}
 \newcommand\vlt[0]{\texttt{l\_t}}
@@ -136,8 +131,6 @@
 \newcommand\news[0]{\texttt{new\_s}}
 \newcommand\newsone[0]{\texttt{new\_s1}}
 \newcommand\newstwo[0]{\texttt{new\_s2}}
-\newcommand\torexpr[0]{\textsf{rexpr}}
-\newcommand\vargs[0]{\texttt{args}}
 \newcommand\newargs[0]{\texttt{new\_args}}
 \newcommand\eqs[0]{\texttt{eqs}}
 \newcommand\neweqs[0]{\texttt{new\_eqs}}
@@ -3223,23 +3216,9 @@ \chapter{Typing of Left-Hand-Side Expressions}
 \item TypingRule.LEConcat (see Section~\ref{sec:TypingRule.LEConcat}).
 \end{itemize}
 
-Some of the rules for left-hand side expressions re-use the annotation rules for right-hand side expressions.
-This is achieved by treating left-hand side expressions as corresponding right-hand side expressions,
-as defined by the recursive function $\torexpr : \lexpr \rightarrow \expr$:
-\[
-\begin{array}{lcl}
-  \textbf{Left hand side expression} & & \textbf{Right hand side expression}\\
-  \hline
-  \torexpr(\texttt{LE\_Var}(\vx)) &=& \texttt{E\_Var}(\vx)\\
-  \torexpr(\leslice(\vle, \vargs)) &=& \texttt{E\_Slice}(\torexpr(\vle), \vargs)\\
-  \torexpr(\texttt{LE\_SetArray}(\vle, \ve)) &=& \texttt{E\_GetArray}(\torexpr(\vle), \ve)\\
-  \torexpr(\texttt{LE\_SetField}(\vle, \vx)) &=& \texttt{E\_GetField}(\torexpr(\vle), \vx)\\
-  \torexpr(\texttt{LE\_SetFields}(\vle, \vx)) &=& \texttt{E\_GetFields}(\torexpr(\vle), \vx)\\
-  \torexpr(\texttt{LE\_Discard}) &=& \texttt{E\_Var("-")}\\
-  \torexpr(\texttt{LE\_Destructuring}([\vle_{1..k}])) &=& \texttt{E\_Tuple}([i=1..k: \torexpr(\vle_i)])\\
-  \torexpr(\texttt{LE\_Concat}([\vle_{1..k}], \Ignore)) &=& \texttt{E\_Concat}([i=1..k: \torexpr(\vle_i)])\\
-\end{array}
-\]
+Some of the rules require viewing left-hand-side expressions as their corresponding right-hand side expressions.
+The correspondence is defined in the ASL Syntax Reference~\cite[Chapter 5]{ASLAbstractSyntaxReference}
+and given by the function $\torexpr : \lexpr \rightarrow \expr$.
 
 \section{TypingRule.LEDiscard \label{sec:TypingRule.LEDiscard}}
 
diff --git a/asllib/doc/ASLmacros.tex b/asllib/doc/ASLmacros.tex
index 7421644a67..ea0b9c4e17 100644
--- a/asllib/doc/ASLmacros.tex
+++ b/asllib/doc/ASLmacros.tex
@@ -147,10 +147,17 @@
 
 \newcommand\identifier[0]{\textsf{identifier}}
 
+\newcommand\vx[0]{\texttt{x}}
+\newcommand\ve[0]{\texttt{e}}
+\newcommand\vle[0]{\texttt{le}}
+\newcommand\vargs[0]{\texttt{args}}
+\newcommand\torexpr[0]{\textsf{rexpr}}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %% Typing macros
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \newcommand\tstruct[0]{\texttt{get\_structure}}
+\newcommand\astlabel[0]{\textsf{ast\_label}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/asllib/instrumentation.ml b/asllib/instrumentation.ml
index 05d3421ea6..079e211bae 100644
--- a/asllib/instrumentation.ml
+++ b/asllib/instrumentation.ml
@@ -62,6 +62,7 @@ module SemanticsRule = struct
     | LESetField
     | LESetFields
     | LEDestructuring
+    | Slices
     | SliceSingle
     | SliceLength
     | SliceRange
@@ -155,6 +156,7 @@ module SemanticsRule = struct
     | LEDestructuring -> "LEDestructuring"
     | LEUndefIdentV0 -> "LEUndefIdentV0"
     | LEUndefIdentV1 -> "LEUndefIdentV1"
+    | Slices -> "Slices"
     | SliceSingle -> "SliceSingle"
     | SliceLength -> "SliceLength"
     | SliceRange -> "SliceRange"
@@ -283,6 +285,7 @@ module SemanticsRule = struct
       Block;
       Loop;
       For;
+      Slices;
     ]
 
   let all_nb = List.length all
diff --git a/asllib/tests/ASLSemanticsReference.t/SemanticsRule.EGetArrayTooSmall.asl b/asllib/tests/ASLSemanticsReference.t/SemanticsRule.EGetArrayTooSmall.asl
index 84c02c35b2..24289cd1fa 100644
--- a/asllib/tests/ASLSemanticsReference.t/SemanticsRule.EGetArrayTooSmall.asl
+++ b/asllib/tests/ASLSemanticsReference.t/SemanticsRule.EGetArrayTooSmall.asl
@@ -1,12 +1,9 @@
 type MyArrayType of array [3] of integer;
 
-var my_array : MyArrayType;  
+var my_array : MyArrayType;
 
 func main () => integer
 begin
-
   my_array[3]=42;
-  assert my_array[3]==42;
-
   return 0;
-end 
+end
diff --git a/asllib/tests/ASLSemanticsReference.t/SemanticsRule.Lit.asl b/asllib/tests/ASLSemanticsReference.t/SemanticsRule.Lit.asl
index 973feb4f7d..b43aa65677 100644
--- a/asllib/tests/ASLSemanticsReference.t/SemanticsRule.Lit.asl
+++ b/asllib/tests/ASLSemanticsReference.t/SemanticsRule.Lit.asl
@@ -1,7 +1,4 @@
 func main () => integer
 begin
-
-  assert 3 == 3;
-  return 0; 
-
+  return 3;
 end
diff --git a/asllib/tests/ASLSemanticsReference.t/run.t b/asllib/tests/ASLSemanticsReference.t/run.t
index 159fbbba6a..fddce12e68 100644
--- a/asllib/tests/ASLSemanticsReference.t/run.t
+++ b/asllib/tests/ASLSemanticsReference.t/run.t
@@ -5,6 +5,7 @@ Hello world should work:
 
 ASL Semantics Reference:
   $ aslref SemanticsRule.Lit.asl
+  [3]
   $ aslref SemanticsRule.ELocalVar.asl
   $ aslref SemanticsRule.EGlobalVar.asl
   $ aslref SemanticsRule.EGlobalVarError.asl
@@ -30,7 +31,7 @@ ASL Semantics Reference:
   $ aslref SemanticsRule.ECall.asl
   $ aslref SemanticsRule.EGetArray.asl
   $ aslref SemanticsRule.EGetArrayTooSmall.asl
-  File SemanticsRule.EGetArrayTooSmall.asl, line 8, characters 2 to 10:
+  File SemanticsRule.EGetArrayTooSmall.asl, line 7, characters 2 to 10:
   ASL Typing error: a subtype of integer {0..(3 - 1)} was expected,
     provided integer {3}.
   [1]
@@ -142,4 +143,3 @@ ASL Semantics Reference:
   [1]
   $ aslref SemanticsRule.LEDiscard.asl
   $ aslref SemanticsRule.LDDiscard.asl
-