Pascal Weisenburger, Johannes Wirth, and Guido Salvaneschi. 2020. A Survey of Multitier Programming. *ACM Comput. Surv.* 53, 4 (2020), 81:1–81:35. https://doi.org/10.1145/3397495

Bill Wilder. 2012. *Cloud architecture patterns: using microsoftazure*. "O'Reilly Media, Inc.".

Derek Wyatt. 2013. *Akka Concurrency*. Artima Incorporation, Sunnyvale, CA, USA.
# A PROJECTION TO JAVA

## A.1 Projection

We omit modifiers (MD) and annotations (AN), they are rendered by the projection as they are.

( Enum ) ( enum id @ A { id } ) = ( enum id { id }

(Interface) ( interface id @ (A) < FTP > extends TE & TE { MDef ; } ) = [ interface name ( id , A , A ) < ( FTP ) > extends ( TE ) A & < ( TE ) A { ( MDef ) A ; } | A ∈ A ]

(Class) ( class id @ (A) < FTP > extends TE implements TE , TE { CField CConst MDef ; MDef { Stm } ) = [ class name ( id , A , A ) extends ( TE ) A implements ( TE ) A , ( TE ) A { ( CField ) A ( CConst ) A ( MDef ) A ; ( MDef ) A { ( ( Stm ) A ) } } | A ∈ A ]

( FTP ) ( id @ (A) extends TE , TE ) = { [ id _A extends ( TE ) A & ( TE ) A | A ∈ A ] if | A | ≥ 1 id extends ( TE ) A otherwise

( TE ) ( void ) A = void

( id @ (B) < TE > ) A =      id < ( TE ) A > B = A id _A' < ( TE ) A > A is the i-th element of B and roleName ( id , i ) = A' Unit otherwise

( MDef ) ( < FTP > TE id ( TE id ) ) A = ( < FTP > ( TE ) A id ( < TE id > )

( CField ) ( TE id ; ) A =      ( TE ) A id ; if A ∈ rolesOf ( TE ) [ blank ] otherwise

( CConst ) ( id ( TE id ) { Stm } ) A = id _A ( < TE id > ) A { ( ( Stm ) A ) }

( Stm ) ( nil ) A = ( [ blank ] ) A = [ blank ] ( return Exp ; ) A = return ( Exp ) A ;

( Exp ; Stm ) A =      switch ( ( Exp ) A ) { case id 3 -> { ( Stm ) A } default -> { throw ... } ( Exp ) A ; ( Stm ) A ( Stm ) A if typeOf ( Exp ) < : Enum @ A , Exp = Exp ' . < TE > id 1 ( id 2 @ A '. id 3 ) and @SelectionMethod ∈ annotOf ( id 1 ) if A ∈ rolesOf ( Exp ) otherwise

( TE id =Exp ; Stm ) A =      ( TE ) A = ( Exp ) A ; ( Stm ) A if A ∈ rolesOf ( TE ) ( Exp ) A ; ( Stm ) A if A ∈ rolesOf ( Exp ) \ rolesOf ( TE ) ( Stm ) A otherwise

( Exp 1 . AsgOp Exp 2 ; Stm ) A =      ( Exp 1 ) A AsgOp ( Exp 2 ) A ; ( Stm ) A if A ∈ rolesOf ( typeOf ( Exp )) ( Exp 1 ) A . id ( ( Exp 2 ) A ) ; ( Stm ) A if A ∈ rolesOf ( Exp 1 , Exp 2 ) ( Stm ) A otherwise

( if ( Exp ) { Stm 1 } else { Stm 2 } Stm ) A =
$$ \begin{cases} \text{if}((\text{Exp})^A)\{((\text{Stm}_1)^A)\} & \text{else}\{((\text{Stm}_2)^A)\} \\ ((\text{Exp})^A); \{[((\text{Stm}_1)^A)] \cup [((\text{Stm}_2)^A)]\} & \text{if typeOf(Exp) = boolean@A} \end{cases} $$

$$ ((\{\text{Stm}_1\}\text{Stm}_2)^A) = ((\{\text{Stm}_1\}^A)\{\text{Stm}_2\}^A) $$

$$ ((\text{try}\{\text{Stm}\}\text{catch}(\text{TE id})\{\text{Stm}\} \text{Stm})^A = \text{try}\{((\text{Stm})^A)\}\overline{\text{catch}(\text{TE id})\{\text{Stm}\}}^A ((\text{Stm})^A) $$

$$ ((\text{catch}(\text{TE id})\{\text{Stm}\})^A = \begin{cases} \text{catch}((\text{TE})^A \text{id})\{((\text{Stm})^A)\} & \text{if } A \in \text{rolesOf}(\text{TE}) \\ [\text{blank}] & \text{otherwise} \end{cases} $$

$$ ((\text{Exp})\text{lit})^A = \begin{cases} l & \text{if } lit = l@(\bar{B}) \text{ and } A \in \bar{B} \\ \text{Unit.id} & \text{otherwise} \end{cases} $$

$$ ((\text{Exp BinOp Exp'})^A) = \begin{cases} ((\text{Exp})^A \text{BinOp} ((\text{Exp'})^A) & \text{if } \begin{cases} \text{BinOp} \in \{\&\&, \mid|\mid\} \\ \wedge \text{rolesOf}(\text{Exp'}) = \{A\} \end{cases} \\ \vee & \begin{cases} \text{BinOp} \notin \{\&\&, \mid|\mid\} \\ \wedge A \in \text{rolesOf}(\text{typeOf}(\text{Exp})) \end{cases} \\ \text{Unit.id}((\text{Exp})^A, ((\text{Exp'})^A) & \text{if } \begin{cases} \text{BinOp} \in \{\&\&, \mid|\mid\} \\ \wedge \text{rolesOf}(\text{Exp'}) = \{A'\} \end{cases} \\ \vee & \text{BinOp} \notin \{\&\&, \mid|\mid\} \end{cases} $$

$$ \text{let head}(\text{Exp}.\text{Exp'}) = \text{Exp}_h, \text{rest}(\text{Exp}.\text{Exp'}) = \text{Exp}_r $$

$$ ((\text{Exp}.\text{Exp'})^A) = \begin{cases} ((\text{Exp}_h)^A \cdot \text{id}((\text{Exp}_r)^A)) & \text{if } ((\text{Exp}_h)^A \in \{\text{Unit}.\bullet\}) \\ \text{Unit.id}((\text{Exp}_h)^A) \cdot \text{Exp}_1 & \text{if } ((\text{Exp}_r)^A \in \{\text{Unit}.\overline{\text{Exp}_1}\}) \\ ((\text{Exp}_h)^A \cdot \text{Exp}_r)^A & \text{otherwise} \end{cases} $$

$$ ((\langle\overline{\text{TE}}\rangle\text{id}(\overline{\text{Exp}}))^A) = \begin{cases} \langle(\overline{\text{TE}})^A\rangle\text{id}(\overline{\langle(\text{Exp})^A\rangle}) & \text{if } A \in \text{rolesOf}(\text{typeOf}(\langle\overline{\text{TE}}\rangle\text{id}(\overline{\text{Exp}}))) \\ \text{Unit.id}(\overline{\langle(\text{Exp})^A\rangle}) & \text{otherwise} \end{cases} $$

$$ ((\text{id@}(\bar{B})).\langle\overline{\text{TE}}\rangle\text{id}(\overline{\text{Exp}}))^A = \begin{cases} \langle\text{id@}(\bar{B})\rangle^A \cdot \langle(\overline{\text{TE}})^A\rangle\text{id}(\overline{((\text{Exp})^A)}) & A \in \bar{B} \\ \text{Unit.id}(\overline{((\text{Exp})^A)}) & \text{otherwise} \end{cases} $$

$$ ((\text{new}\langle\overline{\text{TE}}\rangle\text{id}\langle\overline{\text{TE}}\rangle(\overline{\text{Exp}}))^A) = \begin{cases} \text{new}\langle(\overline{\text{TE}})^A\rangle\langle\text{id@}(\bar{B})\rangle\langle\overline{\text{TE}}\rangle^A((\overline{\text{Exp}})^A) & A \in \bar{B} \\ \text{Unit.id}((\overline{\text{Exp}})^A) & \text{otherwise} \end{cases} $$

$$ ((\text{FAcc})\text{id})^A = \begin{cases} \text{id} & A \in \text{rolesOf}(\text{id}) \\ \text{Unit.id} & \text{otherwise} \end{cases} $$

$$ ((\text{id@}(\bar{B})).f)^A = \begin{cases} \langle\text{id@}(\bar{B})\rangle^A \cdot f & A \in \text{rolesOf}(f) \\ \text{Unit.id} & \text{otherwise} \end{cases} $$
## A.2 Merging

$$ \Box \overline{\mathit{Stm}} = \Box (\mathit{Stm}_1, \dots, \mathit{Stm}_n) = [[\mathit{Stm}_1]] \sqcup \dots \sqcup [[\mathit{Stm}_n]] $$

Statements

$$ \mathit{return} \ Exp \sqcup \mathit{return} \ Exp' = \mathit{return} \ Exp \sqcup Exp' $$

$$ \mathit{TE} \ id; \ \mathit{Stm} \sqcup \ \mathit{TE} \ id; \ \mathit{Stm}' = \mathit{TE} \ id; \ (\mathit{Stm} \sqcup \ \mathit{Stm}'$$

$$ (\mathit{Exp}_1 \ \mathit{AsgOp} \ \mathit{Exp}_2; \mathit{Stm}) \sqcup (\mathit{Exp}'_1 \ \mathit{AsgOp} \ \mathit{Exp}'_2; \mathit{Stm}') \\ = (\mathit{Exp}_1 \sqcup \mathit{Exp}'_1) \ \mathit{AsgOp} \ (\mathit{Exp}_2 \sqcup \mathit{Exp}'_2); \ (\mathit{Stm} \sqcup \ \mathit{Stm}') $$

$$ (\mathit{Exp}; \mathit{Stm}) \sqcup (\mathit{Exp}'; \mathit{Stm}') = (\mathit{Exp} \sqcup \mathit{Exp}'); (\mathit{Stm} \sqcup \ \mathit{Stm}') $$

$$ \{\mathit{Stm}_1\} \ \mathit{Stm}_2 \sqcup \ \{\mathit{Stm}'_1\} \ \mathit{Stm}'_2 = \{\mathit{Stm}_1 \sqcup \ \mathit{Stm}'_1\} \ (\mathit{Stm}_2 \sqcup \ \mathit{Stm}'_2) $$

$$ \mathit{if}(\mathit{Exp})\{\mathit{Stm}_1\}\mathit{else}\{\mathit{Stm}_2\}\mathit{Stm} \sqcup \mathit{if}(\mathit{Exp}')\{\mathit{Stm}'_1\}\mathit{else}\{\mathit{Stm}'_2\}\mathit{Stm}' \\ = \mathit{if}(\mathit{Exp} \sqcup \mathit{Exp}')\{\mathit{Stm}_1 \sqcup \mathit{Stm}'_1\}\mathit{else}\{\mathit{Stm}_2 \sqcup \mathit{Stm}'_2\}(\mathit{Stm} \sqcup \ \mathit{Stm}') $$

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \mathit{switch} \ (\mathit{Exp})\{ & \mathit{switch} \ (\mathit{Exp})\{ & \mathit{switch} \ (\mathit{Exp} \sqcup \mathit{Exp}')\{ \\ & \mathit{case} \ id_a \rightarrow \{\mathit{Stm}_a\} & \mathit{case} \ id_a \rightarrow \{\mathit{Stm}_a \sqcup \ \mathit{Stm}'_a\} \\ \dots & \dots & \dots \\ \mathit{case} \ id_x \rightarrow \{\mathit{Stm}_x\} & \sqcup & \mathit{case} \ id_x \rightarrow \{\mathit{Stm}'_x\} \\ \mathit{case} \ id_y \rightarrow \{\mathit{Stm}_y\} & & \mathit{case} \ id_y \rightarrow \{\mathit{Stm}_y\} \\ \mathit{default} \rightarrow \{\mathit{Stm}_{d1}\} & & \mathit{case} \ id_z \rightarrow \{\mathit{Stm}_z\} \\ \} \ \mathit{Stm} & \} \ \mathit{Stm}' & \mathit{default} \rightarrow \{\mathit{Stm}_{d2}\} \\ & & \mathit{default} \rightarrow \{\mathit{Stm}_{d1} \sqcup \ \mathit{Stm}_{d2}\} \\ \} \ \mathit{Stm} \sqcup \ \mathit{Stm}' & & \} \ \mathit{Stm} \sqcup \ \mathit{Stm}' \end{array} $$

$$ \begin{array}{l} \mathit{try} \{\mathit{Stm}_1\} \ \overline{\mathit{catch}} \ (\mathit{TE} \ id) \ \{\mathit{Stm}\} \ \mathit{Stm}_2 \sqcup \ \mathit{try} \ \{\mathit{Stm}_3\} \ \overline{\mathit{catch}} \ (\mathit{TE} \ id) \ \{\mathit{Stm}'\} \ \mathit{Stm}_4 \\ = \ \mathit{try} \ \{\mathit{Stm}_1 \sqcup \ \mathit{Stm}_3\} \ \overline{\mathit{catch}} \ (\mathit{TE} \ id) \ \{\mathit{Stm} \sqcup \ \mathit{Stm}'\} \ \mathit{Stm}_2 \sqcup \ \mathit{Stm}_4 \end{array} $$

Expressions

$$ \text{let } \bullet \in \{\text{nil}, [\text{blank}], \text{null}, \text{this}, \text{super}, id\}, \bullet \sqcup \bullet = \bullet $$

$$ \text{let } \bullet \in \{\text{new id } \langle \overline{\mathit{TE}} \rangle, \text{ id } \langle \overline{\mathit{TE}} \rangle \}, \bullet (\overline{\mathit{Exp}}) \sqcup \bullet (\overline{\mathit{Exp}'}') = \bullet (\overline{\mathit{Exp}} \sqcup \mathit{Exp}^{''}) $$

$$ (\mathit{Exp}_1 \ \mathit{BinOp} \ \mathit{Exp}_2) \sqcup (\mathit{Exp}'_1 \ \mathit{BinOp} \ \mathit{Exp}'_2); = (\mathit{Exp}_1 \sqcup \mathit{Exp}'_1) \ \mathit{BinOp} \ (\mathit{Exp}_2 \sqcup \mathit{Exp}'_2) $$

$$ \mathit{Exp}_1 \ \mathit{Exp}_2 \sqcup \mathit{Exp}_3 \ \mathit{Exp}_4 = (\mathit{Exp}_1 \sqcup \mathit{Exp}_3)(\mathit{Exp}_2 \sqcup \mathit{Exp}_4) $$

$$ \text{.id} \sqcup \text{.id} = \text{.id} \quad \text{.id} \langle \overline{\mathit{TE}} \rangle (\overline{\mathit{Exp}}) \sqcup \text{.id} \langle \overline{\mathit{TE}} \rangle (\overline{\mathit{Exp}'}') = \text{.id} \langle \overline{\mathit{TE}} \rangle (\overline{\mathit{Exp}} \sqcup \mathit{Exp}^{''}) $$

$$ \mathit{Exp}_1 \ \mathit{Exp}_2 \sqcup \ \mathit{Exp}_3 \ \mathit{Exp}_4 = (\mathit{Exp}_1 \sqcup \ \mathit{Exp}_3)(\mathit{Exp}_2 \sqcup \ \mathit{Exp}_4) $$
## A.3 Normaliser

Statements

```
[[nil]] = nil      [[return Exp;]] = return [[Exp]];      [[TE id; Stm]] = TE id; [[Stm]]
```

```
[[Exp AsgOp Exp'; Stm]] = [[Exp]] AsgOp [[Exp']; [[Stm]]
```

```
[[{Stm} Stm]] = [[[Stm]]] [[Stm]]
```

```
NOOP(Exp) = [
  [blank]      if Exp ∈ {Unit.id, id.id, this, null}
  Exp          otherwise
]
```

```
[[Exp; Stm]] = [
  [[Stm]]      if NOOP([Exp]) = [blank]
  [[Exp]]; [[Stm]] otherwise
]
```

```
[[if(Exp){Stm₁}else{Stm₂}Stm]] = if([Exp]){{Stm₁}}else{{[Stm₂]}}[Stm]
```

```
[switch(Exp){case id->{Stm} default->Stm'} Stm]
= switch([Exp]) {case id->{{[Stm]}} default->[Stm']} [Stm]
```

```
[try {Stm} catch (TE id) {Stm} Stm] = try {[Stm]} catch (TE id) {[Stm]} [Stm]
```

Expressions

```
[null] = null      [[null]]* = <false, null>      [[this]] = this      [[this]]* = <false, this>
```

```
[id] = id      [[id]]* = <false, id>      let [[id<TE>(Exp)]* = <•, •>, [[id<TE>(Exp)]* = ◦
```

```
let <Exp>* = <•, •>, [[id<TE>(Exp)]* = <•, •>, id<TE>(•)]
```

```
let [[new id<TE>(Exp)]* = <•, •>, [[new id<TE>(Exp)]* = ◦
```

```
let [[Exp]* = <•, •>, [[new id<TE>(Exp)]* = <•, •>, new id<TE>(•)]
```

```
[[Exp BinOp Exp')] = [[Exp]] BinOp [[Exp']]
```

```
let [[Exp.Exp'*] = <•, •>, [[Exp.Exp] = {
  [[ ◦ ]]      if • = true
  ◦            otherwise
}
```

```
[[Exp.Exp'*] = [
  <true, Unit.id(Exp)]
  <true, Exp>
  <false, Unit.id>
  <• ∨ •', •, •']
]
  if Exp.Exp' = Unit.id.id(Exp)
  if Exp.Exp' = Unit.id(Exp)
  if Exp = Unit and [[.Exp'*] = <•, [blank]]
  otherwise, let [[Exp]]* = <•, •>
  and [[.Exp'*] = <•', •']
```

```
[.id]* = <false, .id>      let [[.Exp]]* = <•, •>, [[.id.Exp]]* = <•, .id •>
```

```
let [[Exp]]* = <•, •>, [[.id(Exp)]* = [
  <•, •>, .id(•)]
  if .id ≠ .id
  if NOOP(•) = [blank]
  <•, •>, |•| ≠ |•|, .id(•)]
  otherwise, let NOOP(•) = •
```

```
let [[.id<TE>(Exp)]* = <•, •> and [[.Exp]]* = <•', •',
```

```
[[.id<TE>(Exp).Exp]]* = <•, •', •, •']
```