From 5c17423906e5ed354264c640bd54e02d9d891c86 Mon Sep 17 00:00:00 2001 From: Guillermo Ramos Date: Tue, 24 Jun 2014 00:38:51 +0200 Subject: Detalles --- memoria.tex | 60 ++++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 36 insertions(+), 24 deletions(-) diff --git a/memoria.tex b/memoria.tex index 91cb653..08cfc3d 100755 --- a/memoria.tex +++ b/memoria.tex @@ -392,8 +392,8 @@ aritmética entera, etc., y a menudo son capaces de resolver de forma automátic 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} +\section{Objetivos} +\label{sec:objetivos} Para este trabajo se ha decidido contribuir dentro de lo posible a mejorar el sistema EasyCrypt, desarrollado principalmente en el Instituto IMDEA Software en @@ -448,7 +448,7 @@ distinta índole: La principal aportación de EasyCrypt con respecto a otros demostradores de teoremas como Coq\footnote{\url{http://coq.inria.fr/}} o Isabelle/HOL\footnote{\url{http://isabelle.in.tum.de/}} son todas las -facilidades que proporciona para trabajar concretamente en el ámbito de la +facilidades que proporciona para trabajar, concretamente, en el ámbito de la criptografía. Algunos ejemplos son el soporte a demostraciones basadas en secuencias de juegos, la riqueza de juicios (lógica de Hoare y variantes) o su exhaustiva biblioteca estándar, que define tipos de datos habituales (cadenas de @@ -618,11 +618,11 @@ los más destacables son los dos siguientes: 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/}}. +\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. + OCaml. Se verá con mayor profundidad en la sección + \ref{sec:modif-al-anal-lex}, tras explicar las fases del análisis del + lenguaje. \end{itemize} A fin de cuentas, EasyCrypt es un intérprete: lee un fichero fuente y realiza @@ -646,14 +646,13 @@ 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 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} (AST), 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 @@ -674,45 +673,58 @@ 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{invisbl} = [text width=5em, text centered, minimum height=4em] \tikzstyle{line} = [draw, -latex'] -\tikzstyle{cloud} = [draw, ellipse,fill=green!20, node distance=3cm, +\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm, minimum height=2em] \begin{center} \begin{tikzpicture}[node distance = 3cm, auto] % Nodes - \node [block] (lexer) {EcLexer}; + \node [invisbl] (upper) {}; + \node [block, below of=upper] (lexer) {EcLexer}; \node [block, below of=lexer] (parser) {EcParser}; \node [block, below of=parser] (typing) {EcTyping}; - \node [invisbl, below of=typing] (resto) {...}; + \node [invisbl, below of=typing] (lower) {...}; \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); + (upper) edge [] node {\textbf{Código fuente}} (lexer) + (lexer) edge [] node {\textbf{Tokens} (EcParser/EcLexer)} (parser) + (parser) edge [] node {\textbf{AST} (EcParseTree)} (typing) + (typing) edge [] node {\textbf{AST tipado} (EcFol)} (lower); \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 +involucrados en este proceso. 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} +TODO: Menhir, modificaciones en EcLexer + \section{Modificaciones al analizador sintáctico} \label{sec:modif-al-anal-sin} +TODO: Más Menhir, modificaciones en EcParser y EcParseTree + \section{Modificaciones al analizador semántico} \label{sec:modif-al-anal-sem} +TODO: Modificaciones en EcTyping, EcFol, EcEnv, EcScope, EcTheory, EcPV, +EcCommands... :) + +\section{Modificaciones al pretty-printer} +\label{sec:modif-al-anal-sem} + +TODO: Modificaciones en EcPrinting + \chapter{DESARROLLO: INTERFAZ WEB} \chapter{RESULTADOS Y CONCLUSIONES} -- cgit v1.2.3