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} \]
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{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} \]
Operators
\[ \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 \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} \]
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(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{C \vdash e \Rightarrow \texttt{Boolean} \quad C \vdash \mathit{block}_1 : C \quad C \vdash \mathit{block}_2 : C}{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} \]
Contract formation
\[ \frac{C \vdash e \Rightarrow \texttt{Boolean}}{C \vdash (\mathit{label} : e) \;\mathbf{assertion}} \tag{4.21} \]
\[ \frac{C \vdash f \Rightarrow \tau \quad f \in \mathit{fields}(C, \text{current class})}{C^{\mathsf{ensure}} \vdash \texttt{old}\; f \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} \]
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} \]
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 s_1(\ell) = o \quad o.f = v}{s, E \vdash e.f \Rightarrow v,\, 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}}{s, E \vdash e\,?.f \Rightarrow s_1(\ell).f,\, s_1} \tag{5.9} \]
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}) \\ 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} \]
Object creation and constructors
\[ \frac{\begin{array}{c} \ell \;\text{fresh} \quad o_0 = \mathit{initial}(A[\bar\tau]) \quad s_0 = s + \{\ell \mapsto o_0\} \\ 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} \]
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}{s, E \vdash e_1.f := e_2 \Rightarrow E,\; s_2\langle \ell.f \mapsto v\rangle} \tag{5.18} \]
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} \]