1 files changed, 129 insertions, 19 deletions
diff --git a/memoria.tex b/memoria.tex
index 68322d9..91cb653 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -8,6 +8,10 @@
 \usepackage[pagebackref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref}
 \usepackage{perpage}
 
+\usepackage{tikz}
+
+\usetikzlibrary{shapes,arrows}
+
 \input{defs}
 \input{portada/defs}
 
@@ -379,13 +383,14 @@ anteriormente como el de la inducción sobre listas (list_ind) o la definición
 
 Una táctica que vale la pena destacar es \rawec{smt}, que intenta resolver el
 objetivo actual de la demostración invocando \textbf{resolvedores}
-(\textit{solvers}) \textbf{SMT}(<<Satisfiability Modulo Theories>>). Estas
-herramientas están diseñadas para intentar encontrar soluciones a fórmulas
-expresadas en lógica de primer orden, permitiendo ciertas interpretaciones
-adicionales sobre los símbolos. Normalmente soportan ciertas teorías muy útiles
-en criptografía como arrays, listas, aritmética entera, etc., y a menudo son
-capaces de resolver de forma automática partes repetitivas y tediosas de las
-demostraciones, liberando de esa carga de trabajo al criptógrafo.
+\textbf{SMT}(<<Satisfiability Modulo Theories>>) (ver sección
+\ref{sec:arqu-de-easycrypt}). Estas herramientas están diseñadas para intentar
+encontrar soluciones a fórmulas expresadas en lógica de primer orden,
+permitiendo ciertas interpretaciones adicionales sobre los símbolos. Normalmente
+soportan ciertas teorías muy útiles en criptografía como arrays, listas,
+aritmética entera, etc., y a menudo son capaces de resolver de forma automática
+partes repetitivas y tediosas de las demostraciones, liberando de esa carga de
+trabajo al criptógrafo.
 
 \section{Motivación y objetivos}
 \label{sec:motiv-y-objet}
@@ -587,21 +592,126 @@ de su implementación.
 \section{Arquitectura de EasyCrypt}
 \label{sec:arqu-de-easycrypt}
 
-EasyCrypt es un programa complejo, y antes de poder modificarlo hay que entender
-qué partes lo integran y cómo está organizado a nivel de código.
+EasyCrypt está escrito en el lenguaje de programación
+OCaml\footnote{\url{http://ocaml.org/}}, que forma parte de la familia ML de
+lenguajes especialmente diseñados para el desarrollo de demostraciones. La
+unidad de compilación básica de OCaml es el \textbf{módulo}, consistente en un
+fichero de implementación con extensión \textbf{.ml} y un fichero de interfaz
+con extensión \textbf{.mli} donde se declaran las funciones, tipos, etc. La
+compilación es relativamente compleja y se automatiza con ayuda de GNU
+Make\footnote{\url{http://www.gnu.org/software/make/}} y
+ocamlbuild\footnote{\url{http://caml.inria.fr/pub/docs/manual-ocaml-400/manual032.html}}.
+
+EasyCrypt usa varios programas externos para llevar a cabo ciertas tareas, pero
+los más destacables son los dos siguientes:
 
-\begin{enumerate}
-\item Lexer
-\item Parser
-\item AST
-\item ...
-\end{enumerate}
+\begin{itemize}
+\item
+  \textbf{Resolvedores SMT}. Existen multitud de programas que deciden la
+  satisfacibilidad de instancias SMT. Como ya se dijo anteriormente, una
+  instancia de fórmula SMT está expresada en lógica de primer orden y tiene
+  interpretaciones en teorías como los números reales, vectores, bits,
+  etc. Durante una demostración en EasyCrypt se pueden invocar estos
+  resolvedores para tratar de encontrar una solución que satisfaga el objetivo
+  actual usando la táctica \rawec{smt}. Internamente, EasyCrypt estará
+  comunicándose con uno o varios resolvedores y obteniendo la respuesa al
+  problema, si es que existe. Para contar con una única interfaz de
+  programación ante la diversidad de resolvedores, EasyCrypt usa la plataforma
+  \textbf{Why3}\footnote{\url{http://why3.lri.fr/}}.
+\item
+  \textbf{Menhir}\footnote{\url{http://gallium.inria.fr/~fpottier/menhir/}}.
+  Menhir es una biblioteca para generar analizadores léxicos y sintácticos en
+  OCaml. Volveremos a esto una vez hayamos introducido las fases del análisis
+  del lenguaje a continuación.
+\end{itemize}
 
-% ProofGeneral
-% EasyCrypt
-% Why3
-% Solvers
+A fin de cuentas, EasyCrypt es un intérprete: lee un fichero fuente y realiza
+acciones en función de su contenido. Por ello, el componente fundamental es el
+\textbf{analizador del lenguaje}, cuya tarea es transformar el código fuente
+(secuencia de caracteres) en un árbol sintáctico abstracto anotado con
+información de tipos, o mostrar un error y finalizar en caso de que el programa
+esté mal formado.
+
+El análisis del lenguaje consta de varias fases encargadas de abordar niveles
+de abstracción distintos. Conceptualmente, las fases de análisis son las
+siguientes:
+
+\begin{itemize}
+\item \textbf{Análisis léxico}
+Esta fase es la primera que se lleva a cabo y la que tiene un menor nivel de
+abstracción; su entrada es el propio fichero fuente. Durante el análisis léxico
+se transforma la secuencia de caracteres que forma el código fuente en unidades
+mínimas de información (\textbf{tokens}): número, cadena de caracteres,
+identificador, comentario, inicio de bloque, etc. La salida de esta fase es una
+lista conteniendo todos los tokens que describen el programa original, formando
+una estructura de datos muy simple pero más sencilla de recorrer y manejar.
+
+\item \textbf{Análisis sintáctico}
+Durante esta fase se transforma la lista de tokens generada durante el análisis
+léxico en el denominado \textbf{árbol sintáctico abstracto}, una estructura de
+datos que contiene la estructura sintáctica del código fuente. Este analizador
+está especificado por la gramática formal del lenguaje (gramáticas libres de
+contexto, por lo general), cuyas reglas determinan el algoritmo a seguir durante
+la construcción del árbol sintáctico.
+L
+\item \textbf{Análisis semántico/contextual}
+Durante esta fase se recorre el árbol sintáctico generado previamente y se anota
+con información de tipos, se construye la tabla de símbolos y se comprueba que
+el programa, además de estar bien formado sintácticamente, tiene sentido
+semánticamente.
+\end{itemize}
 
+EasyCrypt implementa cada una de estas etapas en tres módulos (EcLexer, EcParser
+y EcTyping) y define las estructuras de datos intermedias en otros dos
+(EcParseTree para el árbol sintáctico abstracto y EcFol para el árbol sintáctico
+anotado con información de tipos). Los módulos EcLexer y EcParser hacen uso de
+la biblioteca Menhir mencionada anteriormente para generar los
+analizadores. Estos módulos contienen las definiciones de tokens y las reglas de
+las gramáticas regular y libre de contexto usadas para indicar, respectivamente,
+el comportamiento de los analizadores léxico y sintáctico.
+
+El siguiente diagrama resume el proceso de análisis del lenguaje de EasyCrypt:
+
+\tikzstyle{block} = [rectangle, draw, fill=blue!20,
+    text width=5em, text centered, rounded corners, minimum height=4em]
+\tikzstyle{invisbl} = [
+    text width=5em, text centered, rounded corners, minimum height=4em]
+\tikzstyle{line} = [draw, -latex']
+\tikzstyle{cloud} = [draw, ellipse,fill=green!20, node distance=3cm,
+    minimum height=2em]
+
+\begin{center}
+\begin{tikzpicture}[node distance = 3cm, auto]
+    % Nodes
+    \node [block] (lexer) {EcLexer};
+    \node [block, below of=lexer] (parser) {EcParser};
+    \node [block, below of=parser] (typing) {EcTyping};
+    \node [invisbl, below of=typing] (resto) {...};
+    \node [cloud, left of=lexer] (menhir1) {Menhir};
+    \node [cloud, left of=parser] (menhir2) {Menhir};
+    % Edges
+    \path [line,dashed] (menhir1) -- (lexer);
+    \path [line,dashed] (menhir2) -- (parser);
+    \path [line]
+    (lexer) edge [] node {\textbf{Tokens} (en EcParser/EcLexer)} (parser)
+    (parser) edge [] node {\textbf{AST} (en EcParseTree)} (typing)
+    (typing) edge [] node {\textbf{AST tipado} (en EcFol)} (resto);
+\end{tikzpicture}
+\end{center}
+
+Para la implementación del coste es necesario modificar cada uno de los módulos
+involucrados en esta cadena. A continuación analizaremos cada una de las etapas
+de la implementación tanto del operador especial de coste como del axioma de
+coste.
+
+\section{Modificaciones al analizador léxico}
+\label{sec:modif-al-anal-lex}
+
+\section{Modificaciones al analizador sintáctico}
+\label{sec:modif-al-anal-sin}
+
+\section{Modificaciones al analizador semántico}
+\label{sec:modif-al-anal-sem}
 
 \chapter{DESARROLLO: INTERFAZ WEB}