This appendix gathers, in one place and without commentary, the inference rules
stated across Chapters 4 and 5. Each rule keeps the tag it carries in the
chapter that introduces it, so a reference such as (4.12) or (5.10) resolves here
as well as there. The chapters give the prose that motivates each rule and a
worked example of its effect; what follows is the formal account in full, for the
reader implementing the language or reasoning about it.
D.1Conformance
The conformance relation \(\tau \preceq \tau'\) of Section 4.3, of which a
type checker computes the reflexive, transitive closure.
General
\[ \tau \preceq \tau \tag{C-Refl} \]
\[ \frac{\tau \preceq \tau' \quad \tau' \preceq \tau''}{\tau \preceq \tau''} \tag{C-Trans} \]
\[ \tau \preceq \mathsf{Any} \tag{C-Top} \]
Inheritance
\[ \frac{A[\alpha_1,\dots,\alpha_n] \;\text{inherits}\; B[\sigma_1,\dots,\sigma_m]}{A[\tau_1,\dots,\tau_n] \preceq B[\sigma_1,\dots,\sigma_m][\tau_i/\alpha_i]} \tag{C-Inherit} \]
Refinement
A refinement type conforms to its base (widening is free); the reverse
narrowing is not a conformance but a checked coercion (Sections 4.3
and 5.6).
\[ \frac{\text{declare type}\; R = B \;\text{where}\; n\,{:}\,p}{R \preceq B} \tag{C-Refine} \]
Optional types
\[ \tau \preceq \tau\,? \tag{C-Opt} \]
\[ \mathsf{Nil} \preceq \tau\,? \tag{C-Nil} \]
\[ \frac{\tau \preceq \tau'}{\tau\,? \preceq \tau'\,?} \tag{C-OptMono} \]
Function types
Parameters vary contravariantly, the result covariantly.
\[ \frac{\tau_i \preceq \sigma_i \;(1 \le i \le n) \quad \sigma \preceq \tau}{\sigma_1 \times \cdots \times \sigma_n \to \sigma \;\preceq\; \tau_1 \times \cdots \times \tau_n \to \tau} \tag{C-Fun} \]
\[ (\tau_1 \times \cdots \times \tau_n \to \tau) \preceq \mathsf{Fun} \tag{C-FunTop} \]
D.2Static Elaboration
The judgement \(C \vdash e \Rightarrow \tau\) (expressions, Section 4.4),
\(C \vdash \mathit{stmt} \Rightarrow C'\) (statements, Section 4.5), and the
auxiliary judgements for contracts and generics (Sections 4.6–4.7).
Constants and variables
\[ C \vdash \mathit{int} \Rightarrow \texttt{Integer} \tag{4.1} \]
\[ C \vdash \mathit{byte} \Rightarrow \texttt{Byte} \tag{4.1a} \]
\[ C \vdash \mathit{int16} \Rightarrow \texttt{Integer16} \tag{4.1b} \]
\[ C \vdash \mathit{int32} \Rightarrow \texttt{Integer32} \tag{4.1c} \]
\[ C \vdash \mathit{real} \Rightarrow \texttt{Real} \tag{4.2} \]
\[ C \vdash \mathit{string} \Rightarrow \texttt{String} \tag{4.3} \]
\[ C \vdash \mathit{char} \Rightarrow \texttt{Char} \tag{4.4} \]
\[ C \vdash \texttt{true} \Rightarrow \texttt{Boolean} \qquad C \vdash \texttt{false} \Rightarrow \texttt{Boolean} \tag{4.5} \]
\[ C \vdash \texttt{nil} \Rightarrow \mathsf{Nil} \tag{4.6} \]
\[ \frac{C(x) = \tau}{C \vdash x \Rightarrow \tau} \tag{4.7} \]
\[ \frac{C(\texttt{this}) = A \quad \{B : A\,\text{inherits}\,B\} = \{P\}}{C \vdash \texttt{super} \Rightarrow P} \tag{4.7a} \]
\[ \frac{C(\texttt{this}) = A \quad A \preceq B \quad B \ne A}{C \vdash B \Rightarrow B} \tag{4.7b} \]
Operators
In rule (4.8), “numeric” means one of \(\texttt{Integer}\), \(\texttt{Byte}\),
\(\texttt{Integer16}\), \(\texttt{Integer32}\), \(\texttt{Real}\), and \(\tau_1 \sqcup \tau_2\)
is \(\texttt{Real}\) if either operand type is \(\texttt{Real}\) and \(\texttt{Integer}\) otherwise
(Section 4.3).
\[ \frac{C \vdash e_1 \Rightarrow \tau_1 \quad C \vdash e_2 \Rightarrow \tau_2 \quad \tau_1,\tau_2 \;\text{numeric}}{C \vdash e_1 \odot e_2 \Rightarrow \tau_1 \sqcup \tau_2} \tag{4.8} \]
\[ \frac{C \vdash e_1 \Rightarrow \tau_1 \quad C \vdash e_2 \Rightarrow \tau_2 \quad \tau_1 \;\text{not numeric} \quad \mathrm{alias}_{\tau_1}(\odot) = m \quad \tau_1 \vdash m : \tau_a \to \tau_r \quad \tau_2 \preceq \tau_a}{C \vdash e_1 \odot e_2 \Rightarrow \tau_r} \tag{4.8a} \]
\[ \frac{C \vdash e_1 \Rightarrow \tau_1 \quad C \vdash e_2 \Rightarrow \tau_2 \quad (\tau_1 \preceq \tau_2 \;\text{or}\; \tau_2 \preceq \tau_1)}{C \vdash e_1 = e_2 \Rightarrow \texttt{Boolean}} \tag{4.9} \]
\[ \frac{C \vdash e_1 \Rightarrow \texttt{Boolean} \quad C \vdash e_2 \Rightarrow \texttt{Boolean}}{C \vdash e_1 \;\texttt{and}\; e_2 \Rightarrow \texttt{Boolean}} \tag{4.10} \]
Member access and calls
\[ \frac{C \vdash e \Rightarrow A[\bar\tau] \quad f : \sigma \in \mathit{fields}(C, A[\bar\tau])}{C \vdash e.f \Rightarrow \sigma} \tag{4.11} \]
\[ \frac{\begin{array}{c}C \vdash e \Rightarrow A[\bar\tau] \quad \mathit{routine}(C, A[\bar\tau], m) = (\sigma_1 \times \cdots \times \sigma_n \to \sigma) \\ C \vdash e_i \Rightarrow \rho_i \quad \rho_i \preceq \sigma_i \;\; (1 \le i \le n)\end{array}}{C \vdash e.m(e_1,\dots,e_n) \Rightarrow \sigma} \tag{4.12} \]
Object creation
\[ \frac{\begin{array}{c} A \;\text{not deferred} \quad k \in \mathit{constructors}(C, A) \quad k : \sigma_1 \times \cdots \times \sigma_n \to A[\bar\tau] \\ C \vdash e_i \Rightarrow \rho_i \quad \rho_i \preceq \sigma_i \;\;(1 \le i \le n) \end{array}}{C \vdash \texttt{create}\; A[\bar\tau].k(e_1,\dots,e_n) \Rightarrow A[\bar\tau]} \tag{4.13} \]
\[ \frac{\begin{array}{c} C(\texttt{this}) = A \quad A \ne P \quad A \preceq P \quad k \in \mathit{ownConstructors}(P) \quad k : \sigma_1 \times \cdots \times \sigma_n \to P \\ C \vdash e_i \Rightarrow \rho_i \quad \rho_i \preceq \sigma_i \;\;(1 \le i \le n) \end{array}}{C \vdash P.k(e_1,\dots,e_n) \Rightarrow C} \tag{4.13a} \]
ownConstructors(\(P\)) is \(P\)’s own
constructor set, declared directly in \(P\) — unlike
constructors(\(C, A\)) in (4.13), which also admits one \(A\) merely
inherits. (4.13a) never binds a name, so it produces \(C\) unchanged, in the
manner of a statement (Section 4.5) even though it is written with
call syntax.
Conditional and anonymous-function expressions
\[ \frac{C \vdash e \Rightarrow \texttt{Boolean} \quad C \vdash e_1 \Rightarrow \tau_1 \quad C \vdash e_2 \Rightarrow \tau_2}{C \vdash \texttt{when}\; e \;\texttt{then}\; e_1 \;\texttt{else}\; e_2 \;\texttt{end} \Rightarrow \tau_1 \sqcup \tau_2} \tag{4.14} \]
\[ \frac{C \oplus \{x_i : \sigma_i\} \vdash \mathit{block} : \sigma}{C \vdash \texttt{fn}\,(x_1{:}\sigma_1,\dots,x_n{:}\sigma_n){:}\sigma\;\texttt{do}\;\mathit{block}\;\texttt{end} \Rightarrow \sigma_1 \times \cdots \times \sigma_n \to \sigma} \tag{4.15} \]
Statements
\[ \frac{C \vdash e \Rightarrow \tau \quad \tau \preceq \sigma \quad x : \notin C}{C \vdash \texttt{let}\; x{:}\sigma := e \Rightarrow C \oplus \{x : \sigma\}} \tag{4.16} \]
\[ \frac{C \oplus \{x : \sigma\} \vdash e \Rightarrow \tau \quad \tau \preceq \sigma \quad x \notin C \quad e = \texttt{fn}\ldots}{C \vdash \texttt{let}\; x{:}\sigma := e \Rightarrow C \oplus \{x : \sigma\}} \tag{4.16'} \]
\[ \frac{C(x) = \sigma \quad C \vdash e \Rightarrow \tau \quad \tau \preceq \sigma \quad x \;\text{not a}\; \texttt{once}\;\text{field outside a constructor}}{C \vdash x := e \Rightarrow C} \tag{4.17} \]
\[ \frac{\begin{array}{c} C \vdash e \Rightarrow B \quad f : \sigma \in \mathit{fields}(C, B) \quad \mathit{declaredBy}(B, f) = A \quad C(\texttt{this}) = A \\ C \vdash e' \Rightarrow \tau \quad \tau \preceq \sigma \end{array}}{C \vdash e.f := e' \Rightarrow C} \tag{4.17a} \]
fields(\(C, B\)) is the same function (4.11) draws \(f\)’s
type from; declaredBy(\(B, f\)) is the one class among \(B\) and its
ancestors whose own feature section introduces \(f\) — \(A\) itself
when \(f\) is not inherited, an ancestor of \(A\) when it is. (4.17a) applies
to this.f := e', super.f := e', and the bare
f := e' alike (the last is (4.17a), not (4.17), exactly when
\(f\) does not satisfy (4.17)’s own \(C(x) = \sigma\) premise from an
enclosing let or parameter first — ordinary shadowing,
tried in that order).
(4.16′) is (4.16)’s exception for a closure-literal value: \(x\)
is visible while \(e\) itself is elaborated, so a closure so bound may call
itself, and a run of consecutive closure-literal lets in one
block are elaborated together so that any of them may call any other —
the closure-literal analogue of §4.8’s free-function rule. Withdrawn,
falling back to (4.16), for a name introduced a second time within reach of
the closures involved (§4.5, which also notes a REPL implementation gap
for a mutually recursive pair called from a later, separate input than the
one that defined them — a limitation of that interactive session, not
of this rule).
Guard-derived facts. Two partial functions on the shape of a guard
expression \(e\), used by the conditional rule below: \(\mathit{narrow}(C, e)\)
gives the bindings a guard proves when \(e\) evaluates to \(\texttt{true}\), and
\(\mathit{narrow}_{\lnot}(C, e)\) the bindings it proves when \(e\) evaluates to
\(\texttt{false}\). Both are total, falling through to \(\emptyset\) on any
expression shape not listed below. \(\oplus\) is extended to a set of
bindings, \(C \oplus S = \bigcup_{(x:\tau)\in S} C \oplus \{x:\tau\}\), for
\(S\) a set of pairwise-distinct names.
\[ \mathit{narrow}(C, x \mathrel{/\!=} \texttt{nil}) = \{x : \tau\} \quad \text{where}\; C(x) = \tau\,? \tag{4.18a} \]
\[ \mathit{narrow}(C, \texttt{convert}\;e\;\texttt{to}\;x{:}\sigma) = \{x : \sigma\} \tag{4.18b} \]
\[ \mathit{narrow}(C, \texttt{?}\,e\,\texttt{as}\,x) = \{x : \tau\} \quad \text{where}\; C \vdash e \Rightarrow \tau\,? \tag{4.18c} \]
\[ \mathit{narrow}(C, e_1\;\texttt{and}\;e_2) = \mathit{narrow}(C, e_1) \cup \mathit{narrow}(C \oplus \mathit{narrow}(C, e_1),\, e_2) \tag{4.18d} \]
\[ \mathit{narrow}(C, e) = \emptyset \quad \text{otherwise} \tag{4.18e} \]
\[ \mathit{narrow}_{\lnot}(C, x = \texttt{nil}) = \{x : \tau\} \quad \text{where}\; C(x) = \tau\,? \tag{4.18f} \]
\[ \mathit{narrow}_{\lnot}(C, e) = \emptyset \quad \text{otherwise} \tag{4.18g} \]
\[ \frac{C \vdash e \Rightarrow \texttt{Boolean} \quad C \oplus \mathit{narrow}(C,e) \vdash \mathit{block}_1 : C_1 \quad C \oplus \mathit{narrow}_{\lnot}(C,e) \vdash \mathit{block}_2 : C_2}{C \vdash \texttt{if}\; e \;\texttt{then}\; \mathit{block}_1 \;\texttt{else}\; \mathit{block}_2 \;\texttt{end} \Rightarrow C} \tag{4.18} \]
Type dispatch and exhaustiveness
\[ \frac{\begin{array}{c} C \vdash e \Rightarrow A \quad B_j \preceq A \quad C \oplus \{x_j : B_j\} \vdash \mathit{block}_j : C \;\;(1 \le j \le k)\\ A \;\text{sealed} \;\Rightarrow\; \{B_1,\dots,B_k\} = \mathit{subclasses}(C, A) \;\;\text{or an}\; \texttt{else}\;\text{clause is present} \end{array}}{C \vdash \texttt{match}\; e \;\texttt{of}\; \overline{\texttt{when}\,B_j\,\texttt{as}\,x_j\,\texttt{then}\,\mathit{block}_j}\; \texttt{end} \Rightarrow C} \tag{4.19} \]
Type conversion
\[ \frac{C \vdash e \Rightarrow \tau \quad (\tau \preceq \sigma \;\text{or}\; \sigma \preceq \tau)}{C \vdash \texttt{convert}\; e \;\texttt{to}\; x{:}\sigma \Rightarrow \texttt{Boolean},\;\; C \oplus \{x : \sigma\,?\}} \tag{4.20} \]
Object test
\[ \frac{C \vdash e \Rightarrow \tau\,?}{C \vdash \texttt{?}\,e\,\texttt{as}\,x \Rightarrow \texttt{Boolean}} \tag{4.20a} \]
Contract formation
\[ \frac{C \vdash e \Rightarrow \texttt{Boolean}}{C \vdash (\mathit{label} : e) \;\mathbf{assertion}} \tag{4.21} \]
\[ \frac{C^{\mathsf{fields}} \vdash e \Rightarrow \tau}{C^{\mathsf{ensure}} \vdash \texttt{old}\; e \Rightarrow \tau} \tag{4.22} \]
Generic elaboration
\[ \frac{A[\alpha_1{\to}K_1,\dots,\alpha_n{\to}K_n] \in \Sigma \quad \tau_i \preceq K_i \;\;(1 \le i \le n)}{C \vdash A[\tau_1,\dots,\tau_n] \;\mathbf{type}} \tag{4.23} \]
D.3Dynamic Evaluation
The principal judgement \(s,\,E \vdash e \Rightarrow v,\, s'\) of
Section 5.2 and its statement analogue \(s, E \vdash \mathit{stmt}
\Rightarrow E', s'\); the exceptional outcome is written \(s, E \vdash e
\Rightarrow \mathbf{raise}\;w,\, s'\).
Constants, variables, and the current object
\[ s, E \vdash \mathit{scon} \Rightarrow \mathcal{V}(\mathit{scon}),\, s \tag{5.1} \]
\[ \frac{E(x) = v}{s, E \vdash x \Rightarrow v,\, s} \tag{5.2} \]
\[ s, E \vdash \texttt{this} \Rightarrow E(\texttt{this}),\, s \tag{5.3} \]
\[ \frac{E(\texttt{this}) = \ell \quad \mathit{class}(s(\ell)) = A \quad \{Q : A\,\text{inherits}\,Q\} = \{P\}}{s, E \vdash \texttt{super} \Rightarrow s(\ell).\mathit{parents}(P),\, s} \tag{5.3a} \]
\[ \frac{E(\texttt{this}) = \ell \quad \mathit{class}(s(\ell)) = A \quad \pi = \mathit{reach}(A, P)}{s, E \vdash P \Rightarrow \mathit{follow}(s, \ell, \pi),\, s} \tag{5.3b} \]
\(\mathit{home}\) and \(\mathit{reach}\) (Section 4.9) are static:
computed once, from the class whose text contains the reference, not
recomputed against whatever object happens to fill \(\mathit{this}\) at run
time — which is safe because \(A\), the class read from
\(\mathit{class}(s(\ell))\) here, is always exactly that class. Every rule
that dispatches into an ancestor’s own routine or constructor body
(5.10, 5.10a, 5.11a) rebinds this there to the reference this
section computes, so by the time that body runs, its own this
again names exactly the class its text belongs to — the invariant
holds throughout, not only at the point super or \(P\) is
first evaluated.
Operators
\[ \frac{s, E \vdash e_1 \Rightarrow v_1, s_1 \quad s_1, E \vdash e_2 \Rightarrow v_2, s_2}{s, E \vdash e_1 \odot e_2 \Rightarrow v_1 \mathbin{\widehat\odot} v_2,\, s_2} \tag{5.4} \]
\[ \frac{s, E \vdash e_1 \Rightarrow v_1, s_1 \quad s_1, E \vdash e_2 \Rightarrow v_2, s_2 \quad v_1, v_2 : \texttt{Integer} \quad v_1 \mathbin{\odot_{\mathbb{Z}}} v_2 \notin [-2^{63},\, 2^{63}-1]}{s, E \vdash e_1 \odot e_2 \Rightarrow \mathbf{raise}\;\mathsf{Arithmetic\_Overflow},\, s_2} \tag{5.4a} \]
\[ \frac{s, E \vdash e_1 \Rightarrow v_1, s_1 \quad s_1, E \vdash e_2 \Rightarrow 0, s_2 \quad v_1, v_2 : \texttt{Integer} \quad \odot \in \{\,/,\,\%\,\}}{s, E \vdash e_1 \odot e_2 \Rightarrow \mathbf{raise}\;\mathsf{Division\_by\_Zero},\, s_2} \tag{5.4b} \]
\[ \frac{s, E \vdash e_1 \Rightarrow v_1, s_1 \quad s_1, E \vdash e_2 \Rightarrow v_2, s_2 \quad v_1 : \tau \quad \mathrm{alias}_{\tau}(\odot) = m \quad s_2, E \vdash v_1.m(v_2) \Rightarrow v, s_3}{s, E \vdash e_1 \odot e_2 \Rightarrow v,\, s_3} \tag{5.4c} \]
Short-circuit conjunction and disjunction
\[ \frac{s, E \vdash e_1 \Rightarrow \mathsf{false}, s_1}{s, E \vdash e_1 \;\texttt{and}\; e_2 \Rightarrow \mathsf{false},\, s_1} \tag{5.5} \]
\[ \frac{s, E \vdash e_1 \Rightarrow \mathsf{true}, s_1 \quad s_1, E \vdash e_2 \Rightarrow v, s_2}{s, E \vdash e_1 \;\texttt{and}\; e_2 \Rightarrow v,\, s_2} \tag{5.6} \]
Member access and the safe access
\[ \frac{s, E \vdash e \Rightarrow \ell, s_1 \quad \ell' = \mathit{follow}(s_1, \ell, \mathit{home}(B, f))}{s, E \vdash e.f \Rightarrow s_1(\ell').f,\, s_1} \tag{5.7} \]
\[ \frac{s, E \vdash e \Rightarrow \texttt{nil}, s_1}{s, E \vdash e\,?.f \Rightarrow \texttt{nil},\, s_1} \tag{5.8} \]
\[ \frac{s, E \vdash e \Rightarrow \ell, s_1 \quad \ell \ne \texttt{nil} \quad \ell' = \mathit{follow}(s_1, \ell, \mathit{home}(B, f))}{s, E \vdash e\,?.f \Rightarrow s_1(\ell').f,\, s_1} \tag{5.9} \]
\(B\), here and in (5.18) below, is \(e\)’s static type, fixed once
by elaboration (4.11) rather than recomputed at run time: fields are not
looked up virtually, by the receiver’s actual class, the way
(5.10)’s routines are. \(\mathit{home}(B,f) = \varepsilon\) whenever
\(B\) declares \(f\) directly, so a receiver typed exactly at the declaring
class — in particular this, whenever
\(C(\texttt{this})\) is that same class — makes \(\ell' = \ell\), and
(5.7)/(5.9) specialise to the plain \(s_1(\ell).f\) they generalise.
Calls and dynamic dispatch
\[ \frac{\begin{array}{c} s, E \vdash e \Rightarrow \ell, s_0 \quad s_0(\ell) = o \quad s_{i-1}, E \vdash e_i \Rightarrow v_i, s_i \;\;(1 \le i \le n) \\ \mathit{lookup}(\mathit{class}(o), m, n) = (x_1,\dots,x_n; \mathit{body}) \quad \ell' = \mathit{follow}(s_n, \ell, \mathit{home}(\mathit{class}(o), m)) \\ E' = E_0[\texttt{this} \mapsto \ell',\; x_i \mapsto v_i] \quad s_n, E' \vdash \mathit{body} \Rightarrow \mathit{ret},\, s' \end{array}}{s, E \vdash e.m(e_1,\dots,e_n) \Rightarrow \mathit{ret},\, s'} \tag{5.10} \]
\[ \frac{\begin{array}{c} E(\texttt{this}) = \ell \quad s_{i-1}, E \vdash e_i \Rightarrow v_i, s_i \;\;(1 \le i \le n) \\ \mathit{lookup}(P, m, n) = (x_1,\dots,x_n; \mathit{body}) \quad \ell' = \mathit{follow}(s_n, \ell, P \cdot \mathit{home}(P, m)) \\ E' = E_0[\texttt{this} \mapsto \ell',\; x_i \mapsto v_i] \quad s_n, E' \vdash \mathit{body} \Rightarrow \mathit{ret},\, s' \end{array}}{s, E \vdash P.m(e_1,\dots,e_n) \Rightarrow \mathit{ret},\, s'} \tag{5.10a} \]
Object creation and constructors
\[ \frac{\begin{array}{c} (\mathit{fields}_0, \mathit{parents}_0, s_0') = \mathit{initial}(s, A[\bar\tau]) \quad \ell \;\text{fresh} \quad s_0 = s_0' + \{\ell \mapsto \langle A, \mathit{fields}_0, \mathit{parents}_0\rangle\} \\ s_{i-1}, E \vdash e_i \Rightarrow v_i, s_i \;\;(1 \le i \le n) \\ k = (x_1,\dots,x_n; \mathit{pre}; \mathit{body}; \mathit{post}) \in \mathit{constructors}(A) \\ \mathit{check}(\mathit{pre}) \quad s_n, E[\texttt{this} \mapsto \ell, x_i \mapsto v_i] \vdash \mathit{body} \Rightarrow s' \\ \mathit{check}(\mathit{post}) \quad \mathit{check}(\mathit{invariant}(A)\;\text{at}\;\ell) \end{array}}{s, E \vdash \texttt{create}\; A[\bar\tau].k(e_1,\dots,e_n) \Rightarrow \ell,\, s'} \tag{5.11} \]
\[ \frac{\begin{array}{c} E(\texttt{this}) = \ell \quad \ell' = s(\ell).\mathit{parents}(P) \quad s_{i-1}, E \vdash e_i \Rightarrow v_i, s_i \;\;(1 \le i \le n) \\ k = (x_1,\dots,x_n; \mathit{pre}; \mathit{body}; \mathit{post}) \in \mathit{ownConstructors}(P) \\ \mathit{check}(\mathit{pre}) \quad s_n, E[\texttt{this} \mapsto \ell', x_i \mapsto v_i] \vdash \mathit{body} \Rightarrow s' \quad \mathit{check}(\mathit{post}) \end{array}}{s, E \vdash P.k(e_1,\dots,e_n) \Rightarrow s'} \tag{5.11a} \]
\(\mathit{initial}(s, A[\bar\tau])\) builds the whole nested shape (5.1)
a fresh \(A[\bar\tau]\) needs before any constructor runs, threading the
store through as it goes:
\[ \mathit{initial}(s, A[\bar\tau]) = \big(\{f \mapsto \mathit{default}(\sigma_f)\}_{f:\sigma_f \,\in\, \mathit{ownFields}(A)},\;\; \{P_1 \mapsto \ell_1, \dots, P_k \mapsto \ell_k\},\;\; s_k\big) \]
where \(P_1,\dots,P_k\) are the parents named in \(A\)’s own
inherit clause, in that order; \(s_0 = s\); and for each
\(i\) in turn, \((\mathit{fields}_i, \mathit{parents}_i, s_i') =
\mathit{initial}(s_{i-1}, P_i[\dots])\), \(\ell_i\) fresh, and
\(s_i = s_i' + \{\ell_i \mapsto \langle P_i, \mathit{fields}_i,
\mathit{parents}_i\rangle\}\) — recursing the same way into each
\(P_i\)’s own parents, and terminating because inheritance is
acyclic. \(\mathit{default}(\sigma)\) is the zero value for a scalar type,
nil for an optional one, and otherwise unattached: Attachment
(Section 4.9) obliges the constructor that runs next to leave nothing
of that shape unattached by the time it returns, but places no such
obligation on \(\mathit{initial}\) itself, which only ever runs with a
constructor call still to come.
Exceptions: raise, rescue, retry
\[ \frac{s, E \vdash e \Rightarrow w, s_1}{s, E \vdash \texttt{raise}\; e \Rightarrow \mathbf{raise}\;w,\, s_1} \tag{5.12} \]
\[ \frac{s, E \vdash \mathit{block}_1 \Rightarrow E_1, s_1}{s, E \vdash \texttt{do}\;\mathit{block}_1\;\texttt{rescue}\;\mathit{block}_2\;\texttt{end} \Rightarrow E, s_1} \tag{5.13} \]
\[ \frac{s, E \vdash \mathit{block}_1 \Rightarrow \mathbf{raise}\;w, s_1 \quad s_1, E[\texttt{exception} \mapsto w] \vdash \mathit{block}_2 \Rightarrow E_2, s_2}{s, E \vdash \texttt{do}\;\mathit{block}_1\;\texttt{rescue}\;\mathit{block}_2\;\texttt{end} \Rightarrow E, s_2} \tag{5.14} \]
\[ \frac{s, E[\texttt{exception} \mapsto w] \vdash \texttt{do}\;\mathit{block}_1\;\texttt{rescue}\;\mathit{block}_2\;\texttt{end} \Rightarrow R, s'}{s, E[\texttt{exception} \mapsto w] \vdash \texttt{retry} \;\text{within}\; \mathit{block}_2 \Rightarrow R, s'} \tag{5.15} \]
Local declaration, assignment, and field update
\[ \frac{s, E \vdash e \Rightarrow v, s_1}{s, E \vdash \texttt{let}\; x := e \Rightarrow E + \{x \mapsto v\},\, s_1} \tag{5.16} \]
\[ \frac{s, E \vdash e \Rightarrow v, s_1}{s, E \vdash x := e \Rightarrow E\langle x \mapsto v\rangle,\, s_1} \tag{5.17} \]
\[ \frac{s, E \vdash e_1 \Rightarrow \ell, s_1 \quad s_1, E \vdash e_2 \Rightarrow v, s_2 \quad \ell' = \mathit{follow}(s_2, \ell, \mathit{home}(B, f))}{s, E \vdash e_1.f := e_2 \Rightarrow E,\; s_2\langle \ell'.f \mapsto v\rangle} \tag{5.18} \]
\(B\) in (5.18) is \(e_1\)’s static type, in the same sense as (5.7)
and (5.9) above. Here it specialises further still: (4.17a) requires
\(C(\texttt{this}) = A\) for a write to type-check at all, where
\(A = \mathit{declaredBy}(B,f)\), so by the time (5.18) runs, the enclosing
method or constructor’s own this already names \(A\)
exactly (Section 5.3), and \(\mathit{home}(B,f)\) is empty whenever
\(e_1\) is that same this: a field is written only ever
“at home,” on the object level that declares it, never reached
from further out.
Conditionals and loops
\[ \frac{s, E \vdash \mathit{init} \Rightarrow E_1, s_1 \quad s_1, E_1 \vdash \texttt{loop}_{u,b} \Rightarrow E', s'}{s, E \vdash \texttt{from}\;\mathit{init}\;\texttt{until}\;u\;\texttt{do}\;b\;\texttt{end} \Rightarrow E', s'} \tag{5.19} \]
\[ \frac{s, E \vdash u \Rightarrow \mathsf{true}, s_1}{s, E \vdash \texttt{loop}_{u,b} \Rightarrow E, s_1} \qquad \frac{s, E \vdash u \Rightarrow \mathsf{false}, s_1 \quad s_1, E \vdash b \Rightarrow E_2, s_2 \quad s_2, E_2 \vdash \texttt{loop}_{u,b} \Rightarrow E', s'}{s, E \vdash \texttt{loop}_{u,b} \Rightarrow E', s'} \tag{5.20} \]