Rephrase TamedFJ intro

tRules.tex

@@ -7,36 +7,48 @@
 % the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
 
 The input to our algorithm is a typeless version of Featherweight Java.
-The syntax is shown in figure \ref{fig:syntax}
-and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
-Method parameters and return types are optional.
-We still require type annotations for fields and generic class parameters.
+The syntax is shown in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
+The respective type rules are defined by figure \ref{fig:expressionTyping} and \ref{fig:typing}.
+\TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
+The point is that a correct and fully typed \TamedFJ{} program is also a correct Featherweight Java program,
+which is vital for our soundness proof (see chapter \ref{sec:soundness}).
+%The language is designed to showcase type inference involving existential types.
+This calculus is used as input aswell as output to our global type inference algorithm.
+We assume that the input to our algorithm is a program, which carries none of the optional type annotations.
+After calculating a type solution we can insert all missing types and generate a correct program.
+
+A method assumption consists out of a method name, a list of type parameters, a list of argument types, and a return type.
+The first argument type is the type of the surrounding class or the \texttt{this} parameter one could say.
+For example the \texttt{add} method in listing \ref{lst:tamedfjSample} is represented by the assumption
+$\texttt{add} : \generics{\ol{X \triangleleft Object}}\ \type{X} \to \exptype{List}{\type{X}}$.
+\begin{lstlisting}[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
+class List<A extends Object> {
+    List<A> add(A v){..,}
+}
+\end{lstlisting}
+%TODO
+\\[1em]
+\noindent
+\textit{Additional Notes:}%
+\begin{itemize}
+\item Method parameters and return types are optional.
+\item We still require type annotations for fields and generic class parameters.
 This is a design choice by us,
 as we consider them as data declarations which are given by the programmer.
 % They are inferred in for example \cite{plue14_3b}
-Note the \texttt{new} expression not requiring generic parameters,
-which are also inferred by our algorithm.
-The method call naturally has type inferred generic parameters aswell.
-We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
-The syntax is described in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
-It is possible to exclude all optional types.
-\TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
-%The language is designed to showcase type inference involving existential types.
-The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program,
-which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}).
-
-\noindent
-\textit{Notes:}
-\begin{itemize}
-\item The calculus does not include method overriding for simplicity reasons.
+\item We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
+\item \textit{Note:} The \texttt{new} expression is not requiring generic parameters.
+\item Every method has an unique name.
+The calculus does not include method overriding for simplicity reasons.
 Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
-%\textit{Note:}
+\item The \textsc{T-Program} type rule ensures that there is one set of method assumptions used for all classes
+that are part of the program.
 \item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
 Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus
 needs to be restricted in that regard.
 Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible
-and as close to it's Featherweight Java correspondent \cite{WildcardsNeedWitnessProtection} as possible.
-Our soundness proof works either way.
+and as close to it's Featherweight Java correspondent as possible,
+simplifying the soundness proof.
 \end{itemize}
 
 %Additional features like overriding methods and method overloading can be added by copying the respective parts from there.