LARA

Tool 2009 Typing Rules and Constraints

The type $TUnit$ is used for elements that need to be type-checked but do not carry a type themselves (this includes statements).

Class definitions and subtyping

  • 1

    \begin{equation*} \frac{\textsf{class}\ ID\ \{ \ldots \} }{ ID \in classes } \end{equation*}

  • 2

    \begin{equation*} \frac{\textsf{class}\ ID_1\ \textsf{extends}\ ID_2\ \{ \ldots \},\ ID_2 \in classes }{ ID_1 \in classes,\ ID_1 <: ID_2 } \end{equation*}

  • 3

    \begin{equation*} \frac{ID \in classes}{ ID <: ID } \end{equation*}

  • 4

    \begin{equation*} \frac{ID \in classes}{ ID <: TObject } \end{equation*}

  • 5

    \begin{equation*} \frac{ID_1 <: ID_2,\ ID_2 <: ID_3}{ ID_1 <: ID_3 } \end{equation*}

  • 6

    \begin{equation*} \frac{A <: B,\ A \neq B,\ B <: A} {\textsf{type error}} \end{equation*}

  • 7

    \begin{equation*} TInt <: TInt \end{equation*}

  • 8

    \begin{equation*} TBoolean <: TBoolean \end{equation*}

  • 9

    \begin{equation*} TString <: TString \end{equation*}

  • 10

    \begin{equation*} TIntArray <: TIntArray \end{equation*}

Class variables and methods

  • 11

    \begin{equation*}\frac{\textsf{class}\ ID\ \{ \textsf{var} f_1 : T_1 ;\ \ldots\ \textsf{var} f_n : T_n;\ \textsf{{d}ef} \ m_1(\ldots): T_{n+1}\ \textsf{=} \{\ldots\}\ \ldots\ \textsf{{d}ef}\ m_k(\ldots): T_{n+k} \textsf{=} \{\ldots\}\ \}}{fields(ID) = \{ (f_i \rightarrow T_i) | 1 \leq i \leq n \}}\end{equation*}

  • 12

    \begin{equation*}\frac{\textsf{class}\ ID\ \textsf{extends}\ ID_2\ \{ \textsf{var} f_1 : T_1 ;\ \ldots\ \textsf{var} f_n : T_n;\ \textsf{{d}ef} \ m_1(\ldots): T_{n+1}\ \textsf{=} \{\ldots\}\ \ldots\ \textsf{{d}ef}\ m_k(\ldots): T_{n+k} \textsf{=} \{\ldots\}\ \}}{fields(ID) = fields(ID_2) \cup \{ (f_i \rightarrow T_i) | 1 \leq i \leq n \}} \end{equation*}

  • 13

    \begin{equation*} \frac{\textsf{class}\ ID\ \{ \textsf{var} f_1 : T_1 ;\ \ldots\ \textsf{var} f_n : T_n;\ \textsf{{d}ef} \ m_1(T_1^1,\ \ldots,\ T_1^{l_1}): T_{n+1}\ \textsf{=} \{\ldots\}\ \ldots\ \textsf{{d}ef} \ m_k(T_k^1,\ \ldots,\ T_k^{l_k}): T_{n+k}\ \textsf{=} \{\ldots\}\ \} }{ methodType(m_j, ID) = (T_j^1 \times \ldots \times \ T_j^{l_j}) \rightarrow T_{n+j}, \forall(1 \leq j \leq k) } \end{equation*}

  • 14

    \begin{equation*} \frac{\textsf{class}\ ID\ \textsf{extends}\ ID_2\ \{ \textsf{var} f_1 : T_1 ;\ \ldots\ \textsf{var} f_n : T_n;\ \textsf{{d}ef} \ m_1(T_1^1,\ \ldots,\ T_1^{l_1}): T_{n+1}\ \textsf{=} \{\ldots\}\ \ldots\ \textsf{{d}ef} \ m_k(T_k^1,\ \ldots,\ T_k^{l_k}): T_{n+k}\ \textsf{=} \{\ldots\}\ \},\ \forall(1 \leq i \leq k):\ m \neq m_i }{ methodType(m, ID) = methodType(m, ID_2) } \end{equation*}

  • 15

    \begin{equation*} \frac{methodType(m, ID_1) \neq methodType(m, ID_2),\ ID_1 <: ID_2}{\textsf{overriding error}} \end{equation*}

Special main object:

  • 16

    \begin{equation*} \frac{\Gamma \vdash stat : TUnit}{\textsf{object}\ ID\ \{ \textsf{{d}ef main() : Unit =} \{ stat \} : TUnit } \end{equation*}

Type-checking method bodies

In class $ID$:

  • 17

    \begin{equation*} \frac{\Gamma \oplus fields(ID) \oplus (\textsf{this} \rightarrow ID) \oplus \{ (v_i \rightarrow T_i) | 1 \leq i \leq n \} \vdash stat_1 : TUnit,\ \ldots,\ stat_l : TUnit,\ e : T_S,\ T_S <: T_R } {\Gamma \vdash \textsf{{d}ef}\ m(v_1:T_1 ,\ \ldots,\ v_k:T_k):T_R\ \{ v_{k+1}:T_{k+1} ;\ \ldots\ v_n:T_n ;\ stat_1;\ \ldots\ stat_l;\ \textsf{return}\ e; \} : TUnit } \end{equation*}

Expressions

  • 18

    \begin{equation*} \frac{\Gamma \vdash e_1 : TBoolean,\ e_2 : TBoolean}{\Gamma \vdash e_1\ \textsf{\&\&}\ e_2 : TBoolean } \end{equation*}

  • 19

    \begin{equation*} \frac{\Gamma \vdash e_1 : TBoolean,\ e_2 : TBoolean}{\Gamma \vdash e_1\ \textsf{$||$}\ e_2 : TBoolean } \end{equation*}

  • 20

    \begin{equation*} \frac{\Gamma \vdash e_1 : TInt,\ e_2 : TInt}{\Gamma \vdash e_1\ \textsf{+}\ e_2 : TInt } \end{equation*}

  • 21

    \begin{equation*} \frac{\Gamma \vdash e_1 : TString,\ e_2 : TInt}{\Gamma \vdash e_1\ \textsf{+}\ e_2 : TString } \end{equation*}

  • 22

    \begin{equation*} \frac{\Gamma \vdash e_1 : TInt,\ e_2 : TString}{\Gamma \vdash e_1\ \textsf{+}\ e_2 : TString } \end{equation*}

  • 23

    \begin{equation*} \frac{\Gamma \vdash e_1 : TString,\ e_2 : TString}{\Gamma \vdash e_1\ \textsf{+}\ e_2 : TString } \end{equation*}

  • 24

    \begin{equation*} \frac{\Gamma \vdash e_1 : TInt,\ e_2 : TInt}{\Gamma \vdash e_1\ \textsf{-}\ e_2 : TInt } \end{equation*}

  • 25

    \begin{equation*} \frac{\Gamma \vdash e_1 : TInt,\ e_2 : TInt}{\Gamma \vdash e_1\ \textsf{/}\ e_2 : TInt } \end{equation*}

  • 26

    \begin{equation*} \frac{\Gamma \vdash e_1 : TInt,\ e_2 : TInt}{\Gamma \vdash e_1\ <\ e_2 : TBoolean } \end{equation*}

  • 27

    \begin{equation*} \frac{\Gamma \vdash e_1 : TBoolean}{\Gamma \vdash \textsf{!}\ e_1 : TBoolean } \end{equation*}

  • 28

    \begin{equation*} \frac{\Gamma \vdash e_1 : TInt,\ e_2 : TInt}{\Gamma \vdash e_1\ \textsf{==}\ e_2 : TBoolean } \end{equation*}

  • 29

    \begin{equation*} \frac{\Gamma \vdash e_1 : TIntArray,\ e_2 : TIntArray}{\Gamma \vdash e_1\ \textsf{==}\ e_2 : TBoolean } \end{equation*}

  • 30

    \begin{equation*} \frac{\Gamma \vdash e_1 : TBoolean,\ e_2 : TBoolean}{\Gamma \vdash e_1\ \textsf{==}\ e_2 : TBoolean } \end{equation*}

  • 31

    \begin{equation*} \frac{\Gamma \vdash e_1 : TString,\ e_2 : TString}{\Gamma \vdash e_1\ \textsf{==}\ e_2 : TBoolean } \end{equation*}

  • 32

    \begin{equation*} \frac{\Gamma \vdash e_1 : ID_1,\ e_2 : ID_2,\ ID_1 \in classes,\ ID_2 \in classes}{\Gamma \vdash e_1\ \textsf{==}\ e_2 : TBoolean } \end{equation*}

  • 33

    \begin{equation*} \frac{\Gamma \vdash e_1 : TIntArray,\ e_2 : TInt}{\Gamma \vdash e_1\textsf{[}e_2\textsf{]} : TInt } \end{equation*}

  • 34

    \begin{equation*} \frac{\Gamma \vdash e_1 : TIntArray}{\Gamma \vdash e_1\textsf{.length} : TInt } \end{equation*}

  • 35

    \begin{equation*} \frac{\Gamma \vdash e_1 : TInt}{\Gamma \vdash \textsf{new Int[}e_1\textsf{]} : TIntArray } \end{equation*}

  • 36

    \begin{equation*} \frac{\Gamma \vdash ID \in classes}{\Gamma \vdash \textsf{new }ID\textsf{()} : ID } \end{equation*}

  • 37

    \begin{equation*} \frac{\Gamma \vdash e_1 : ID,\ ID \in classes,\ \ a_1 : T_1^1,\ \ldots,\ a_n : T_n^1,\ T_1^1 <: T_1^2,\ \ldots,\ T_n^1 <: T_n^2,\ methodType(m, ID) = (T_1^2 \times \ldots \times T_n^2) \rightarrow T_R }{\Gamma \vdash e_1\textsf{.}m\textsf{(}a_1\textsf{, \ldots, }a_n\textsf{)} : T_R } \end{equation*}

  • 38

    \begin{equation*} \frac{n \in \{\ldots,\ -2, -1, 0, 1, 2, \ldots\} }{n : TInt} \end{equation*}

  • 39

    \begin{equation*} \frac{}{\textsf{"string constant"} : TString } \end{equation*}

  • 40

    \begin{equation*} \frac{}{\textsf{true} : TBoolean } \end{equation*}

  • 41

    \begin{equation*} \frac{}{\textsf{false} : TBoolean } \end{equation*}

  • 42

    \begin{equation*} \frac{(id \rightarrow T) \in \Gamma }{\Gamma \vdash id : T } \end{equation*}

Statements

  • 43

    \begin{equation*} \frac{\Gamma \vdash s_1 : TUnit,\ \ldots,\ s_n : TUnit}{\Gamma \vdash \textsf{\{} s_1 \ldots s_n \textsf{\}} : TUnit \end{equation*}

  • 44

    \begin{equation*} \frac{\Gamma \vdash x : TBoolean,\ s : TUnit}{\Gamma \vdash \textsf{if(}x\textsf{)}\ s : TUnit} \end{equation*}

  • 45

    \begin{equation*} \frac{\Gamma \vdash x : TBoolean,\ s_1 : TUnit,\ s_2 : TUnit}{\Gamma \vdash \textsf{if(}x\textsf{)}\ s_1\ \textsf{else}\ s_2 : TUnit} \end{equation*}

  • 46

    \begin{equation*} \frac{\Gamma \vdash x : TBoolean,\ s : TUnit}{\Gamma \vdash \textsf{while(}x\textsf{)}\ s : TUnit} \end{equation*}

  • 47

    \begin{equation*} \frac{\Gamma \vdash x : TBoolean}{\Gamma \vdash \textsf{println(}x\textsf{);} : TUnit \end{equation*}

  • 48

    \begin{equation*} \frac{\Gamma \vdash x : TInt}{\Gamma \vdash \textsf{println(}x\textsf{);} : TUnit \end{equation*}

  • 49

    \begin{equation*} \frac{\Gamma \vdash x : TString}{\Gamma \vdash \textsf{println(}x\textsf{);} : TUnit \end{equation*}

  • 50

    \begin{equation*} \frac{\Gamma \vdash x : T_1,\ y : T_2,\ T_2 <: T_1}{\Gamma \vdash x\ \textsf{=}\ y\textsf{;} : TUnit \end{equation*}

  • 51

    \begin{equation*} \frac{\Gamma \vdash x : TIntArray,\ y : TInt,\ z : TInt}{\Gamma \vdash x\textsf{[}y\textsf{]}\ \textsf{=}\ z\textsf{;} : TUnit \end{equation*}