From f2d883ef69c6ad97e071e036c67732b6825e8193 Mon Sep 17 00:00:00 2001 From: Guillermo Ramos Date: Wed, 25 Jun 2014 19:55:45 +0200 Subject: Usando minted. Tonterías varias --- Makefile | 2 +- lib/minted.sty | 239 +++++++++++++++++++++++++++++++++++++++++++++ memoria.tex | 304 ++++++++++++++++++++++++++++++++++++++------------------- 3 files changed, 444 insertions(+), 101 deletions(-) create mode 100644 lib/minted.sty diff --git a/Makefile b/Makefile index 87124d7..a5a2792 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ all: - latexmk -pvc --pdf -interaction=nonstopmode memoria.tex + latexmk -shell-escape -pvc --pdf -interaction=nonstopmode memoria.tex clean: rm -rf _region_.tex *.aux *.bbl *.blg *.brf *.dvi *.fdb_latexmk *.fls *.fmt *.idx *.log *.lol *.out *.prv *.toc diff --git a/lib/minted.sty b/lib/minted.sty new file mode 100644 index 0000000..0e0585c --- /dev/null +++ b/lib/minted.sty @@ -0,0 +1,239 @@ +%% +%% This is file `minted.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% minted.dtx (with options: `package') +%% Copyright 2010--2011 Konrad Rudolph +%% +%% This work may be distributed and/or modified under the +%% conditions of the LaTeX Project Public License, either version 1.3 +%% of this license or (at your option) any later version. +%% The latest version of this license is in +%% http://www.latex-project.org/lppl.txt +%% and version 1.3 or later is part of all distributions of LaTeX +%% version 2005/12/01 or later. +%% +%% Additionally, the project may be distributed under the terms of the new BSD +%% license. +%% +%% This work has the LPPL maintenance status `maintained'. +%% +%% The Current Maintainer of this work is Konrad Rudolph. +%% +%% This work consists of the files minted.dtx and minted.ins +%% and the derived file minted.sty. +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{minted}[2011/09/17 v1.7 Yet another Pygments shim for LaTeX] +\RequirePackage{keyval} +\RequirePackage{fancyvrb} +\RequirePackage{xcolor} +\RequirePackage{float} +\RequirePackage{ifthen} +\RequirePackage{calc} +\RequirePackage{ifplatform} +\DeclareOption{chapter}{\def\minted@float@within{chapter}} +\DeclareOption{section}{\def\minted@float@within{section}} +\ProcessOptions\relax +\ifwindows + \providecommand\DeleteFile[1]{\immediate\write18{del #1}} +\else + \providecommand\DeleteFile[1]{\immediate\write18{rm #1}} +\fi +\newboolean{AppExists} +\newcommand\TestAppExists[1]{ + \ifwindows + \DeleteFile{\jobname.aex} + \immediate\write18{for \string^\@percentchar i in (#1.exe #1.bat #1.cmd) + do set >\jobname.aex >\jobname.aex} %$ + \newread\@appexistsfile + \immediate\openin\@appexistsfile\jobname.aex + \expandafter\def\expandafter\@tmp@cr\expandafter{\the\endlinechar} + \endlinechar=-1\relax + \readline\@appexistsfile to \@apppathifexists + \endlinechar=\@tmp@cr + \ifthenelse{\equal{\@apppathifexists}{}} + {\AppExistsfalse} + {\AppExiststrue} + \immediate\closein\@appexistsfile + \DeleteFile{\jobname.aex} +\immediate\typeout{file deleted} + \else + \immediate\write18{which #1 && touch \jobname.aex} + \IfFileExists{\jobname.aex} + {\AppExiststrue + \DeleteFile{\jobname.aex}} + {\AppExistsfalse} + \fi} +\newcommand\minted@resetoptions{} +\newcommand\minted@defopt[1]{ + \expandafter\def\expandafter\minted@resetoptions\expandafter{% + \minted@resetoptions + \@namedef{minted@opt@#1}{}}} +\newcommand\minted@opt[1]{ + \expandafter\detokenize% + \expandafter\expandafter\expandafter{\csname minted@opt@#1\endcsname}} +\newcommand\minted@define@opt[3][]{ + \minted@defopt{#2} + \ifthenelse{\equal{#1}{}}{ + \define@key{minted@opt}{#2}{\@namedef{minted@opt@#2}{#3}}} + {\define@key{minted@opt}{#2}[#1]{\@namedef{minted@opt@#2}{#3}}}} +\newcommand\minted@define@switch[3][]{ + \minted@defopt{#2} + \define@booleankey{minted@opt}{#2} + {\@namedef{minted@opt@#2}{#3}} + {\@namedef{minted@opt@#2}{#1}}} +\minted@defopt{extra} +\newcommand\minted@define@extra[1]{ + \define@key{minted@opt}{#1}{ + \expandafter\def\expandafter\minted@opt@extra\expandafter{% + \minted@opt@extra,#1=##1}}} +\newcommand\minted@define@extra@switch[1]{ + \define@booleankey{minted@opt}{#1} + {\expandafter\def\expandafter\minted@opt@extra\expandafter{% + \minted@opt@extra,#1}} + {\expandafter\def\expandafter\minted@opt@extra\expandafter{% + \minted@opt@extra,#1=false}}} +\minted@define@switch{texcl}{-P texcomments} +\minted@define@switch{mathescape}{-P mathescape} +\minted@define@switch{linenos}{-P linenos} +\minted@define@switch{startinline}{-P startinline} +\minted@define@switch[-P funcnamehighlighting=False]% + {funcnamehighlighting}{-P funcnamehighlighting} +\minted@define@opt{gobble}{-F gobble:n=#1} +\minted@define@opt{bgcolor}{#1} +\minted@define@extra{frame} +\minted@define@extra{framesep} +\minted@define@extra{framerule} +\minted@define@extra{rulecolor} +\minted@define@extra{numbersep} +\minted@define@extra{firstnumber} +\minted@define@extra{stepnumber} +\minted@define@extra{firstline} +\minted@define@extra{lastline} +\minted@define@extra{baselinestretch} +\minted@define@extra{xleftmargin} +\minted@define@extra{xrightmargin} +\minted@define@extra{fillcolor} +\minted@define@extra{tabsize} +\minted@define@extra{fontfamily} +\minted@define@extra{fontsize} +\minted@define@extra{fontshape} +\minted@define@extra{fontseries} +\minted@define@extra{formatcom} +\minted@define@extra{label} +\minted@define@extra@switch{numberblanklines} +\minted@define@extra@switch{showspaces} +\minted@define@extra@switch{resetmargins} +\minted@define@extra@switch{samepage} +\minted@define@extra@switch{showtabs} +\minted@define@extra@switch{obeytabs} +\newsavebox{\minted@bgbox} +\newenvironment{minted@colorbg}[1]{ + \def\minted@bgcol{#1} + \noindent + \begin{lrbox}{\minted@bgbox} + \begin{minipage}{\linewidth-2\fboxsep}} + {\end{minipage} + \end{lrbox}% + \colorbox{\minted@bgcol}{\usebox{\minted@bgbox}}} +\newwrite\minted@code +\newcommand\minted@savecode[1]{ + \immediate\openout\minted@code\jobname.pyg + \immediate\write\minted@code{#1} + \immediate\closeout\minted@code} +\newcommand\minted@pygmentize[2][\jobname.pyg]{ + \def\minted@cmd{pygmentize -l #2 -f latex -F tokenmerge + \minted@opt{gobble} \minted@opt{texcl} \minted@opt{mathescape} + \minted@opt{startinline} \minted@opt{funcnamehighlighting} + \minted@opt{linenos} -P "verboptions=\minted@opt{extra}" + -o \jobname.out.pyg #1} + \immediate\write18{\minted@cmd} + % For debugging, uncomment: + %\immediate\typeout{\minted@cmd} + \ifthenelse{\equal{\minted@opt@bgcolor}{}} + {} + {\begin{minted@colorbg}{\minted@opt@bgcolor}} + \input{\jobname.out.pyg} + \ifthenelse{\equal{\minted@opt@bgcolor}{}} + {} + {\end{minted@colorbg}} + \DeleteFile{\jobname.out.pyg}} +\newcommand\minted@usedefaultstyle{\usemintedstyle{default}} +\newcommand\usemintedstyle[1]{ + \renewcommand\minted@usedefaultstyle{} + \immediate\write18{pygmentize -S #1 -f latex > \jobname.pyg} + \input{\jobname.pyg}} +\newcommand\mint[3][]{ + \DefineShortVerb{#3} + \minted@resetoptions + \setkeys{minted@opt}{#1} + \SaveVerb[aftersave={ + \UndefineShortVerb{#3} + \minted@savecode{\FV@SV@minted@verb} + \minted@pygmentize{#2} + \DeleteFile{\jobname.pyg}}]{minted@verb}#3} +\newcommand\minted@proglang[1]{} +\newenvironment{minted}[2][] + {\VerbatimEnvironment + \renewcommand{\minted@proglang}[1]{#2} + \minted@resetoptions + \setkeys{minted@opt}{#1} + \begin{VerbatimOut}[codes={\catcode`\^^I=12}]{\jobname.pyg}}% + {\end{VerbatimOut} + \minted@pygmentize{\minted@proglang{}} + \DeleteFile{\jobname.pyg}} +\newcommand\inputminted[3][]{ + \minted@resetoptions + \setkeys{minted@opt}{#1} + \minted@pygmentize[#3]{#2}} +\newcommand\newminted[3][]{ + \ifthenelse{\equal{#1}{}} + {\def\minted@envname{#2code}} + {\def\minted@envname{#1}} + \newenvironment{\minted@envname} + {\VerbatimEnvironment\begin{minted}[#3]{#2}} + {\end{minted}} + \newenvironment{\minted@envname *}[1] + {\VerbatimEnvironment\begin{minted}[#3,##1]{#2}} + {\end{minted}}} +\newcommand\newmint[3][]{ + \ifthenelse{\equal{#1}{}} + {\def\minted@shortname{#2}} + {\def\minted@shortname{#1}} + \expandafter\newcommand\csname\minted@shortname\endcsname[2][]{ + \mint[#3,##1]{#2}##2}} +\newcommand\newmintedfile[3][]{ + \ifthenelse{\equal{#1}{}} + {\def\minted@shortname{#2file}} + {\def\minted@shortname{#1}} + \expandafter\newcommand\csname\minted@shortname\endcsname[2][]{ + \inputminted[#3,##1]{#2}{##2}}} +\@ifundefined{minted@float@within} + {\newfloat{listing}{h}{lol}} + {\newfloat{listing}{h}{lol}[\minted@float@within]} +\newcommand\listingscaption{Listing} +\floatname{listing}{\listingscaption} +\newcommand\listoflistingscaption{List of listings} +\providecommand\listoflistings{\listof{listing}{\listoflistingscaption}} +\AtBeginDocument{ + \minted@usedefaultstyle} +\AtEndOfPackage{ + \ifnum\pdf@shellescape=1\relax\else + \PackageError{minted} + {You must invoke LaTeX with the + -shell-escape flag} + {Pass the -shell-escape flag to LaTeX. Refer to the minted.sty + documentation for more information.}\fi + \TestAppExists{pygmentize} + \ifAppExists\else + \PackageError{minted} + {You must have `pygmentize' installed + to use this package} + {Refer to the installation instructions in the minted + documentation for more information.} + \fi} +\endinput +%% +%% End of file `minted.sty'. diff --git a/memoria.tex b/memoria.tex index 7b54c31..f14d7db 100755 --- a/memoria.tex +++ b/memoria.tex @@ -9,14 +9,12 @@ \usepackage{perpage} \usepackage{tikz} +\usepackage{lib/minted} \usepackage{float} \floatstyle{boxed} -\newfloat{ocaml}{thp}{ext} - -\usepackage{alltt} -\usepackage{color} -\input{ocaml_colors} +\newfloat{code}{th}{los}[chapter] +\floatname{code}{Listado de código} \usetikzlibrary{shapes,arrows} @@ -31,13 +29,15 @@ \input{portada/portada} \pagenumbering{roman} + \emptypage \chapter*{Resumen} \chapter*{Abstract} -\emptypage +\emptypage \tableofcontents +\emptypage \chapter{INTRODUCCIÓN} \label{cha:introduccion} \pagenumbering{arabic} @@ -91,11 +91,30 @@ considera seguro porque la existencia de un ataque eficiente contra el criptosistema implicaría también la existencia de una forma eficiente de factorizar enteros (que hasta el día de hoy, se desconoce). -\begin{figure}[h] - \centering - \includegraphics[width=0.6\textwidth]{img/proofs.png} - \caption{Construcción de pruebas} - \label{fig:proofs} +\tikzstyle{block} = [rectangle, draw, fill=blue!20, + 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=blue!10, node distance=3cm, +minimum height=2em] + +\begin{figure}[ht] + \centering + \begin{tikzpicture}[node distance = 6cm, auto] + % Nodes + \node [block, fill=blue!40] (primitiva) {Primitiva}; + \node [block, below of=primitiva, fill=blue!40] (esquema) {Esquema}; + \node [block, right of=primitiva, fill=red!60] (ataque1) {Ataque}; + \node [block, right of=esquema, fill=red!60] (ataque2) {Ataque}; + % Edges + \path [line,dashed] (ataque1) -- (primitiva); + \path [line,dashed] (ataque2) -- (esquema); + \path [line] + (primitiva) edge node[left] {\textbf{Construcción}} (esquema) + (ataque2) edge node[right] {\textbf{Reducción}} (ataque1); + \end{tikzpicture} + \caption{Construcción de pruebas} + \label{fig:proofs} \end{figure} \section{Criptografía asimétrica} @@ -185,16 +204,20 @@ secuencias de juegos, como CertiCrypt y su versión mejorada EasyCrypt EasyCrypt es un marco formado por un \textbf{lenguaje de programación} junto a un motor de resolución de \textbf{lógica de Hoare Relacional Probabilística} -(ver sección \ref{sec:juicios}) \cite{BartheGB09}. EasyCrypt funciona como un -intérprete de un lenguaje de propósito general y de forma interactiva: cuando se -le proporciona un fichero fuente a evaluar, lo recorre de arriba hacia abajo -comprobando que todos los pasos de las demostraciones son correctos. Usando -Proof General, un modo del editor de texto Emacs, es posible editar un fichero -fuente mientras el intérprete lo va evaluando sobre la marcha, ayudando y -guiando al usuario a medida que éste desarrolla cada demostración. - -EasyCrypt usa varios lenguajes de programación distintos a la hora de evaluar un -código fuente. A continuación veremos cuáles son, con algunos ejemplos. +(ver sección \ref{sec:juicios}) \cite{BartheGB09}. EasyCrypt es un proyecto de +software libre, distribuido bajo los términos de la licencia CeCILL-B, y su +código fuente está accesible desde la página del +proyecto\footnote{\url{https://www.easycrypt.info/}}. + +EasyCrypt funciona como un intérprete de un lenguaje de propósito general y de +forma interactiva: cuando se le proporciona un fichero fuente a evaluar, lo +recorre de arriba hacia abajo comprobando que todos los pasos de las +demostraciones son correctos. Usando Proof General, un modo del editor de texto +Emacs, es posible editar un fichero fuente mientras el intérprete lo va +evaluando sobre la marcha, ayudando y guiando al usuario a medida que éste +desarrolla cada demostración. EasyCrypt usa varios lenguajes de programación +distintos a la hora de evaluar un código fuente. A continuación veremos cuáles +son, con algunos ejemplos. \subsection{Lenguajes de especificacion} \label{sec:leng-de-espec} @@ -202,7 +225,7 @@ código fuente. A continuación veremos cuáles son, con algunos ejemplos. Estos lenguajes se usan para declarar y definir tipos, funciones, axiomas, juegos, oráculos, adversarios, entidades involucradas en las pruebas, etc. -\paragraph{Lenguaje de expresiones} +\subsubsection{Lenguaje de expresiones} El lenguaje principal de especificación de EasyCrypt es el de las expresiones, que define una serie de \textbf{tipos} (conjuntos de valores) y \textbf{operadores} sobre ellos. En EasyCrypt, siguiendo la notación del cálculo @@ -211,9 +234,9 @@ puntos. Así, (\rawec{b:bool}) denota la pertenencia del valor \rawec{b} al tipo \rawec{bool}. EasyCrypt posee un potente sistema de tipos que soporta polimorfismo y tipos de orden superior. Los tipos de orden superior están parametrizados por otros tipos que se colocan delante: <<\rawec{int - list}>> significa <>. Los tipos se pueden generalizar + list}>> significa ``lista de enteros''. Los tipos se pueden generalizar usando una variable de tipo (variable precedida de una comilla simple): -<<\rawec{'a list}>> significa <>. +<<\rawec{'a list}>> significa ``lista de cualquier tipo''. Los \textbf{operadores} son funciones definidas sobre tipos, y se introducen con la palabra reservada <<\rawec{op}>>: (\rawec{op par : nat -> bool}). La aplicación @@ -254,7 +277,7 @@ satisface el predicado (o \rawec{None} si ninguno lo satisface). Por último, se define un axioma llamado \rawec{find_head}: si dado un elemento \rawec{x} y una lista, siendo \rawec{x} el primer elemento de la lista, se llama -a \rawec{find} con el predicado <>, el resultado deberá ser +a \rawec{find} con el predicado ``igual a \rawec{x}'', el resultado deberá ser (\rawec{Some x}). En EasyCrypt hay dos formas de definir hechos: usando @@ -262,7 +285,7 @@ En EasyCrypt hay dos formas de definir hechos: usando sí mismo, mientras que un lema se debe acompañar de una demostración, como se verá en el apartado \ref{sec:tactics}. -\paragraph{Lenguaje de expresiones probabilísticas} +\subsubsection{Lenguaje de expresiones probabilísticas} Para poder razonar sobre distribuciones de probabilidad, EasyCrypt proporciona un tipo (\rawec{'a distr}) que representa sub-distribuciones discretas sobre \rawec{'a}. La principal herramienta para trabajar sobre sub-distribuciones es @@ -281,7 +304,7 @@ axiom mu_def : forall (p : bool -> bool), (1/2) * charfun p false. \end{easycrypt} -\paragraph{Lenguaje pWhile} +\subsubsection{Lenguaje pWhile} Los lenguajes de expresiones a menudo son inadecuados para definir juegos y otras estructuras de datos como esquemas de cifrado u oráculos, debido a la necesidad de representar algoritmos secuenciales, entidades con estado, @@ -317,7 +340,7 @@ etc. Para ello, EasyCrypt implementa un lenguaje distinto llamado pWhile Estos lenguajes se usan para definir lemas y demostrarlos. -\paragraph{Juicios} +\subsubsection{Juicios} \label{sec:juicios} Los juicios son proposiciones que se pueden realizar en EasyCrypt, y tienen @@ -362,7 +385,7 @@ Hoare que se usan para razonar sobre la ejecución de programas: memoria al ser ejecutado. \end{itemize} -\paragraph{Tácticas} +\subsubsection{Tácticas} \label{sec:tactics} Para demostrar juicios, EasyCrypt cuenta con un lenguaje basado en tácticas @@ -398,7 +421,7 @@ 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} -\textbf{SMT}(<>) (ver sección +\textbf{SMT} (<>) (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 @@ -456,7 +479,7 @@ distinta índole: su utilización en los círculos de gente que se dedica a la criptografía. \end{itemize} -\pagebreak +\emptypage \chapter{DESARROLLO: COSTE} \label{cha:desarrollo:-coste} @@ -490,7 +513,7 @@ TODO referencias a dónde se explica qué. Supongamos que el usuario está construyendo una demostración de que un criptosistema de clave pública es seguro siempre que los recursos del adversario -no sean superiores a cierto límite. En este caso, por <> nos referimos a +no sean superiores a cierto límite. En este caso, por ``seguro'' nos referimos a que el adversario no es capaz de descifrar un texto cifrado sin poseer la clave privada correspondiente. Como hemos visto en la sección \ref{sec:cript-asim}, esto es equivalente a decir que el adversario no es capaz de \textbf{invertir} @@ -682,19 +705,14 @@ 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 comportamiento de los analizadores léxico y sintáctico. Todo este proceso +aparece ilustrado en la figura \ref{fig:ecparser}. -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, minimum height=4em] -\tikzstyle{line} = [draw, -latex'] -\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm, - minimum height=2em] +\tikzstyle{line} = [draw] -\begin{center} -\begin{tikzpicture}[node distance = 3cm, auto] +\begin{figure}[ht] + \centering + \begin{tikzpicture}[node distance = 3cm, auto] % Nodes \node [invisbl] (upper) {}; \node [block, below of=upper] (lexer) {EcLexer}; @@ -704,15 +722,17 @@ El siguiente diagrama resume el proceso de análisis del lenguaje de EasyCrypt: \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] - (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} + \path [line, dashed] (menhir1) -- (lexer); + \path [line, dashed] (menhir2) -- (parser); + \path [line, -latex'] + (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} + \caption{Analizador del lenguaje de EasyCrypt} + \label{fig:ecparser} +\end{figure} Para la implementación del coste es necesario modificar cada uno de los módulos involucrados en este proceso. A continuación analizaremos las etapas de la @@ -741,30 +761,64 @@ contrario, se emite el token genérico IDENT. Por tanto, basta con añadir dos entradas a este hash map para que EcLexer emita los tokens COST y CAXIOM cuando encuentre los identificadores `cost` y `caxiom`, respectivamente: -\begin{ocaml} -\begin{alltt} - -\Clet{let} _keywords \Cnonalphakeyword{=} \Cnonalphakeyword{[} - \Cstring{"admit"} \Cnonalphakeyword{,} \Cconstructor{ADMIT}\Cnonalphakeyword{;} - \Cstring{"forall"}\Cnonalphakeyword{,} \Cconstructor{FORALL}\Cnonalphakeyword{;} - \Cstring{"exists"}\Cnonalphakeyword{,} \Cconstructor{EXIST}\Cnonalphakeyword{;} - \Cstring{"pragma"}\Cnonalphakeyword{,} \Cconstructor{PRAGMA}\Cnonalphakeyword{;} - \Ccomment{(* ... *)} - - \Cstring{"cost"} \Cnonalphakeyword{,} \Cconstructor{COST}\Cnonalphakeyword{;} - \Cstring{"caxiom"}\Cnonalphakeyword{,} \Cconstructor{CAXIOM} -\Cnonalphakeyword{]} - -\Clet{let} keywords \Cnonalphakeyword{=} \Cconstructor{Hashtbl}\Cnonalphakeyword{.}create 100 -\Clet{let} \Cnonalphakeyword{_} \Cnonalphakeyword{=} \Cconstructor{List}\Cnonalphakeyword{.}iter - \Cnonalphakeyword{(}\Cfun{fun} \Cnonalphakeyword{(}x\Cnonalphakeyword{,} y\Cnonalphakeyword{)} \Cnonalphakeyword{->} \Cconstructor{Hashtbl}\Cnonalphakeyword{.}add keywords x y\Cnonalphakeyword{)} _keywords -\end{alltt} -\end{ocaml} +\begin{code} + \begin{minted}{ocaml} +let _keywords = [ +"admit" , ADMIT; +"forall", FORALL; +"exists", EXIST; +"pragma", PRAGMA; +(* ... *) + +"cost" , COST; +"caxiom", CAXIOM +] + +let keywords = Hastbl.create 100 +let _ = List.iter (fun x, y -> Hashtbl.add keywords x y) _keywords + \end{minted} + \caption{ecLexer.mll} +\end{code} \section{Modificaciones al analizador sintáctico} \label{sec:modif-al-anal-sin} -TODO: Más Menhir, modificaciones en EcParser y EcParseTree +Una vez el analizador léxico reconoce las nuevas palabras reservadas que hemos +introducido, es tarea del analizador sintáctico reconocer las estructuras que +forman los tokens. El analizador sintáctico de EasyCrypt está implementado en el +módulo EcParser que, al igual que el analizador léxico, no se define usando +código OCaml normal: el fichero que lo contiene es <>, y debe ser +procesado por Menhir para generar el auténtico analizador sintáctico. + +La función de este módulo es la especificación de la gramática de EasyCrypt como +tal. Esto se realiza describiendo las reglas en formato BNF <>. La sintaxis concreta que usa Menhir es la siguiente: + +\newpage +\lstset{ + literate=% + {á}{{\'a}}1 + {é}{{\'e}}1 + {í}{{\'i}}1 + {ó}{{\'o}}1 + {ú}{{\'u}}1 +} +\begin{lstlisting}[frame=lrtb] + : + | [] { } + | [] { } + | ... +\end{lstlisting} + +Cada regla define un símbolo no terminal ($<$nombre_regla$>$) que la identifica, +así como uno o varios \textbf{grupos de producción} que representan las posibles +expansiones de la regla. Cada grupo de producción comienza por el símbolo de la +barra vertical <<$\vert$>>, continúa con una serie de símbolos que pueden hacer +referencia a tokens o a otras reglas, y termina con una expresión entre llaves +<<\{ , \}>> conteniendo las \textbf{acciones semánticas} de la regla (los +efectos secundarios que se llevan a cabo durante su expansión). + +TODO: modificaciones en EcParser y EcParseTree \section{Modificaciones al analizador semántico} \label{sec:modif-al-anal-sem} @@ -777,6 +831,7 @@ EcCommands... :) TODO: Modificaciones en EcPrinting +\emptypage \chapter{DESARROLLO: INTERFAZ WEB} Como ya mencionamos en la sección \ref{sec:objetivos}, EasyCrypt es un programa @@ -793,13 +848,7 @@ navegador. La mayor inspiración que tenemos para el diseño es el del propio Proof General, que es con lo que se trabaja en EasyCrypt normalmente: -// -\\ -\\ -// [screenshot de Emacs + ProofGeneral] -\\ -\\ -// +// [TODO screenshot de Emacs + ProofGeneral] En nuestro caso, la parte fundamental de la interfaz será el editor de código fuente. Los resultados de la evaluación del código se mostrarán a la derecha del @@ -812,7 +861,7 @@ puede ver el primer prototipo de la página principal de la web\footnote{A pesar formulario de creación de cuentas de usuario, etc.), en este documento no se mencionarán por no ser tan relevantes en su interacción con EasyCrypt.}. -\begin{figure}[h] +\begin{figure}[ht] \centering \includegraphics[width=0.8\textwidth]{img/web-prototype.png} \caption{Diseño de la web} @@ -869,23 +918,19 @@ web básicas (HTML, CSS, JavaScript), más tediosas y propensas a error: \textbf{Tornado}\footnote{\url{http://www.tornadoweb.org//}}. \end{itemize} -Todas estas partes se integran entre sí tal y como se muestra en el siguiente -esquema: +La integración de todas estas partes se ilustra en la figura \ref{fig:warch}. -\tikzstyle{block} = [rectangle, draw, fill=blue!20, - text width=5em, text centered, rounded corners, minimum height=4em] -\tikzstyle{line} = [draw] -\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm, - minimum height=2em] \tikzstyle{ncloud} = [draw, ellipse,fill=blue!10, node distance=2cm, - minimum height=2em] +minimum height=2em] -\begin{center} -\begin{tikzpicture}[node distance = 6cm, auto] +\begin{figure}[ht] + \centering + \begin{tikzpicture}[node distance = 6cm, auto] % Nodes - \node [block] (client) {Cliente}; - \node [block, right of=client] (wserver) {Servidor web}; - \node [block, below of=wserver, node distance=4cm] (ecserver) {Servidor EasyCrypt}; + \node [block] (wserver) {Servidor web}; + \node [invisbl, below of=wserver, node distance = 2cm] (dummy) {}; + \node [block, below of=dummy, node distance=2cm] (ecserver) {Servidor EasyCrypt}; + \node [block, left of=dummy] (client) {Cliente}; \node [ncloud, above of=client] (bootstrap) {Twitter Bootstrap}; \node [cloud, left of=client] (jquery) {jQuery}; @@ -909,19 +954,75 @@ esquema: \path [line,dashed] (tornado) -- (ecserver); \path [line] - (client) edge [] node {\textbf{HTTP}} (wserver) - (client) edge [] node {\textbf{WebSockets}} (ecserver); -\end{tikzpicture} -\end{center} + (client) edge node[sloped, anchor=center, above] {\textbf{HTTP}} (wserver) + (client) edge node[sloped, anchor=center, above] {\textbf{WebSockets}} (ecserver); + \end{tikzpicture} + \caption{Arquitectura de la interfaz web} + \label{fig:warch} +\end{figure} A continuación veremos cómo se ha implementado cada uno de estos componentes y formado el sistema completo. -\section{Implementación: cliente} +\section{Implementación: servidor web} -TODO +Como ya hemos visto, el servidor web está implementado en Django +(Python). Django sigue el patrón modelo-vista-controlador (MVC), por lo que nos +centraremos en cada una de estas partes por separado para tener una idea +general de la implementación. -\section{Implementación: servidor web} +\subsection{Modelo} +\label{sec:modelo} + +El modelo es el esquema general de los datos que se van a manejar en la +aplicación. En este caso va a ser muy simple, ya que los únicos datos que se van +a manipular son \textbf{proyectos} y \textbf{ficheros}. Normalmente también +necesitaríamos entidades como <> para implementar la autenticación, +pero Django proporciona esa funcionalidad en una de sus bibliotecas estándares. + +Nuestras entidades serán las siguientes: + +\begin{itemize} +\item Entidad: \textbf{Project} + \begin{itemize} + \item Atributo: \textbf{name} (tipo: string) + \item Atributo: \textbf{owner} (tipo: User) + \end{itemize} +\item Entidad: \textbf{File} + \begin{itemize} + \item Atributo: \textbf{name} (tipo: string) + \item Atributo: \textbf{contents} (tipo: string) + \item Atributo: \textbf{project} (tipo: Project) + \end{itemize} +\end{itemize} + +Es decir, cada usuario (User) posee uno o varios proyectos (Project), que a su +vez contienen uno o varios ficheros (File). + +En Django los modelos de datos se almacenan en un fichero especial +<>. Cada entidad se representa como una clase de Python, y los +atributos del modelo son atributos de instancia: + +\begin{code} + \begin{minted}{python} +class Project(models.Model): + name = models.CharField(max_length=200) + owner = models.ForeignKey(get_user_model()) + # ... + +class File(models.Model): + name = models.CharField(max_length=200) + contents = models.TextField() + project = models.ForeignKey(Project) + # ... + \end{minted} +\end{code} + +\subsection{Vista} + +\subsection{Controlador} + +\section{Implementación: cliente} TODO @@ -929,10 +1030,13 @@ TODO TODO +\emptypage \chapter{RESULTADOS Y CONCLUSIONES} +\emptypage \chapter{CONTRIBUCIONES} +\emptypage \chapter{ANEXOS} \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr} -- cgit v1.2.3