The expression new C(args) allocates one location per field of the whole chain of C, the root base first, then the tagged record, and runs the constructors from the root base down, each with this bound to the object, the one of C with the arguments and the others with none, since there are no initialiser lists.

A class without a constructor is created by new C() and keeps the default values.

\dfrac{C \mapsto \mathtt{class}\ C\ \{\ldots C(p_1\,x_1, \ldots, p_k\,x_k)\ \{c\} \ldots\} \qquad \text{arguments as in T-Call}}{\Gamma \vdash \mathtt{new}\ C(e_1, \ldots, e_k) : C*}\;\textsf{(T-New)}

\dfrac{\begin{array}{c} f_1 \ldots f_n \text{ the fields of the chain of } C\qquad (\ell_i, \sigma_i) = \mathrm{alloc}(\sigma_{i-1}, \mathrm{default}\,\tau_i) \\ (\ell, \sigma') = \mathrm{alloc}(\sigma_n, \mathsf{obj}\,C\,[f_1 \mapsto \ell_1, \ldots, f_n \mapsto \ell_n]) \\ \text{the constructors of the chain run from the root down} \\ \text{with } \mathtt{this} \mapsto \ell \text{, giving } \sigma'' \end{array}}{\rho, \sigma \vdash \mathtt{new}\ C(e_1, \ldots, e_k) \Rightarrow \mathsf{loc}\,\ell, \sigma''}\;\textsf{(New)}

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

The call of a member body, a method, a constructor or a destructor, binds this to the location \ell of the receiver as an alias and the parameters as in the call of a function, by value with a fresh copy and by reference with an alias. The return frees the copies and the locals of the body, never the receiver.

\dfrac{\begin{array}{c} p_i = \tau_i \Rightarrow \rho, \sigma'_{i-1} \vdash e_i \Rightarrow v_i, \sigma_i,\ (\ell_i, \sigma'_i) = \mathrm{alloc}(\sigma_i, v_i) \\ p_i = \tau_i\& \Rightarrow \rho, \sigma'_{i-1} \vdash e_i \Rightarrow_{\ell} \ell_i, \sigma'_i \\ \rho_m = [\mathtt{this} \mapsto \ell, x_1 \mapsto \ell_1, \ldots, x_k \mapsto \ell_k]\qquad \rho_m, \sigma'_k \vdash c \Rightarrow r, \rho', \sigma'' \end{array}}{\mathrm{member}\ \ell\ (e_1, \ldots, e_k) \Rightarrow v, \sigma'' \setminus (\{\ell_i \mid p_i \text{ by value}\} \cup (\rho' \setminus \rho_m))}\;\textsf{(Member)}

With \mathsf{normal} in place of \mathsf{ret}\,v the result is \mathsf{void} for a void member and error otherwise.

The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

A method call e.m(args) needs a receiver of class type and e->m(args) a receiver of pointer type. The method is the nearest m in the chain of the static class of the receiver, it must be visible, and the arguments are checked as in a call. An unqualified call m(args) inside a member body is this->m(args).

\dfrac{\begin{array}{c} \Gamma \vdash e : C\qquad C \text{ has } \tau\ m(p_1\,x_1, \ldots, p_k\,x_k) \text{ visible from } \Gamma \\ \text{arguments as in T-Call} \end{array}}{\Gamma \vdash e.m(e_1, \ldots, e_k) : \tau}\;\textsf{(T-Method)}

\dfrac{\begin{array}{c} \Gamma \vdash e : C*\qquad C \text{ has } \tau\ m(\ldots) \text{ visible from } \Gamma \\ \text{arguments as in T-Call} \end{array}}{\Gamma \vdash e\mathtt{->}m(e_1, \ldots, e_k) : \tau}\;\textsf{(T-MethodArrow)}

\dfrac{\begin{array}{c} \rho, \sigma \vdash e \Rightarrow_{\ell} \ell, \sigma_0 \text{ or } \rho, \sigma \vdash e \Rightarrow \mathsf{loc}\,\ell, \sigma_0\qquad \sigma_0(\ell) = \mathsf{obj}\,T\,[\ldots] \\ S \text{ the static class of } e \\ m \mapsto \tau\ m(\ldots)\{c\} \text{ nearest } S \text{, or nearest } T \text{ when virtual} \\ \mathrm{member}\ \ell\ (e_1, \ldots, e_k) \Rightarrow v, \sigma' \end{array}}{\rho, \sigma \vdash e.m(e_1, \ldots, e_k) \Rightarrow v, \sigma'}\;\textsf{(MethodCall)}

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.