\SPLC{} is a program written in the purely functional lazy programming language
Clean\footnote{\url{http://clean.cs.ru.nl/Clean}}. \SPLC{} has a standardized
UNIX like command line interface and functions as a filter in a way that it
-processes standard input in standard output. Default command line argument such
+processes standard input to standard output. Default command line argument such
as \texttt{--version} and \texttt{--help} provide the expected output. To
illustrate all the command line interface options the output of \texttt{spl
--help} is given in Listing~\ref{lst:splchelp}.
%A concise but precise description of how the work was divided amongst the
%members of
%the team.
+
+The semantic analysis phase asses if a -grammatically correct- program is also
+semantically correct and decorates the program with extra information it
+finds during this checking. The input of the semantic analysis is an \AST/ of
+the
+parsed program, its output is either a semantically correct and completely typed
+\AST/ plus the environment in which it was typed (for debug purposes), or it is
+an error describing the problem with the \AST/.
+
+During this analysis \SPLC checks four properties of the program:
+\begin{enumerate}
+ \item That no functions are declared with the same name
+ \item That \tt{main} is of type \tt{(-> Void)}
+ \item That the program includes a main function
+ \item That the program is correctly typed
+\end{enumerate}
+The first three steps are simple sanity checks which are coded in slightly over
+two dozen lines of Clean code. The last step is a Hindley Milner type inference
+algorithm, which is a magnitude more complex. This last step also decorates the
+\AST/ with inferred type information.
+
+\subsection{Sanity checks}
+The sanity checks are defined as simple recursive functions over the function
+declarations in the AST. We will very shortly describe them here.
+
+\begin{description}
+ \item [No duplicate functions] This function checks that the program does
+ not contain top level functions sharing the same name. Formally:
+ $ \forall f \in \textrm{functions} \ldotp \neg
+ \exists g \in \textrm{functions} \setminus \{f\} \ldotp
+ f.\textrm{name} = g.\textrm{name}$
+ \item [\tt{main} should have type \tt{->Void}] Our semantics of \SPL{}
+ require the main function to take no arguments and to not return a
+ value. Formally: $\forall f \in \textrm{functions} \ldotp
+ f.\textrm{name} = \textrm{'main'} \Rightarrow
+ \textit{typeof}\textrm{(main)} = \rightarrow\textrm{Void} $
+ \item [The program should have a main function] $\exists f \in
+ \textrm{functions} \ldotp f.\textrm{name} = \textrm{'main'}$
+\end{description}
\ No newline at end of file