First commit

This commit is contained in:
zapashcanon 2017-09-10 22:53:20 +02:00
commit d17754ef6b
Signed by: zapashcanon
GPG Key ID: 8981C3C62D1D28F1
27 changed files with 854 additions and 0 deletions

0
CHANGELOG.md Normal file
View File

16
LICENSE.md Normal file
View File

@ -0,0 +1,16 @@
The ISC License (ISC)
=====================
Copyright (c) 2017, Léo Andrès
Permission to use, copy, modify, and/or distribute this software for any
purpose with or without fee is hereby granted, provided that the above
copyright notice and this permission notice appear in all copies.
THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

13
Makefile Normal file
View File

@ -0,0 +1,13 @@
default: build clean
build:
scripts/build.sh
clean:
scripts/clean.sh
test:
scripts/test.sh
mrproper: clean
scripts/mrproper.sh

0
README.md Normal file
View File

BIN
img/bluebanner.jpg Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 40 KiB

BIN
img/greenbanner.jpg Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 70 KiB

203
img/i.pdf Normal file

File diff suppressed because one or more lines are too long

BIN
img/logoCNRS-en.pdf Normal file

Binary file not shown.

BIN
img/logoCNRS-fr.pdf Normal file

Binary file not shown.

BIN
img/logoCNRS.pdf Normal file

Binary file not shown.

BIN
img/logoINRIA-en.pdf Normal file

Binary file not shown.

BIN
img/logoINRIA-fr.pdf Normal file

Binary file not shown.

BIN
img/logoLRI.pdf Normal file

Binary file not shown.

BIN
img/logoUPS.pdf Normal file

Binary file not shown.

BIN
img/redbanner.jpg Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 35 KiB

BIN
img/yellowbanner.jpg Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 38 KiB

302
includes/poster.sty Normal file
View File

@ -0,0 +1,302 @@
%****************************************
% Style for LRI posters
% Michel Beaudouin-Lafon (mbl@lri.fr)
% v0.1 20nov2008
%****************************************
\ProvidesPackage{lriposter}[2008/11/20 v0.1 ]
\NeedsTeXFormat{LaTeX2e}
%---------- Page geometry ------------------------------
\usepackage{geometry}
\geometry{paper=a3paper,left=1cm,right=1cm,top=0.5cm,bottom=0.5cm}
%---------- Fonts and special characters ------------------------------
% change fonts: see packages psnfss & psnfssx
\usepackage[T1]{fontenc}
%---------- Basic packages ------------------------------
\usepackage{calc}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage{multicol} % to have parts of the document in multicolumns
\usepackage{fancybox} % to create framed text
%---------- General settings ------------------------------
% --- IMPORTANT ---
% the caller MUST have defined the \templatedir variable with the path to the template.
% the default value for the layout of the SVN repository would be:
% \def\templatedir{../../templates/lri2008}
% \usepackage{\templatedir/lriposter}
% the directory holding the template images.
\def\Poster@ImageDir{\templatedir/img}
% the width of the banner and the fotter (a bit wider than the main text)
\newlength\bannerwidth\setlength\bannerwidth{\textwidth + 1cm}
% emphasized text is set in \emphcolor
\renewcommand{\emph}[1]{{\color{\emphcolor}\textbf{#1}}}
% paragraphs are not indented and are separated by 2ex
\setlength\parskip{2ex plus 0.2ex minus 0.2ex}
\setlength\parindent{0pt}
% some useful colors
\definecolor{lrilogored}{RGB}{200,50,46}
\definecolor{lrilogoyellow}{RGB}{236,216,182}
\definecolor{lrilogogreen}{RGB}{160,162,130}
\definecolor{lrilogogray}{RGB}{130,131,132}
\definecolor{lrired}{rgb}{0.64,0.25,0.23}% burgundy
\definecolor{lriblue}{RGB}{58,80,135}% concord blue
\definecolor{lrigreen}{RGB}{90,122,109}% olive green
\definecolor{lriyellow}{RGB}{237,230,204}% sand
%\definecolor{lribrown}{RGB}{163,137,91}
% attempts at getting some kind of gold color for the yellow template...
%\definecolor{lrigold}{RGB}{193,160,4}
%\definecolor{lrigold}{RGB}{199,173,95}
%\definecolor{lrigold}{RGB}{255,208,110}
%\definecolor{lrigold}{RGB}{240,194,104}
%\definecolor{lrigold}{RGB}{240,184,64}
%\definecolor{lrigold}{RGB}{231,200,122}
%\definecolor{lrigold}{RGB}{223,193,118}
%\definecolor{lrigold}{RGB}{220,149,17}
\definecolor{lrigold}{RGB}{217,147,17}
\definecolor{gray}{cmyk}{0,0,0,0.6}
\definecolor{lightgray}{cmyk}{0,0,0,0.15}
%%\definecolor{lrired}{RGB}{68,121,119}% for banner4 - green
%%\definecolor{lrired}{RGB}{90,122,133}% for banner4 - french blue
% define the banner image
\newcommand{\posterbanner}[1]{
\gdef\Poster@Banner{\Poster@ImageDir/#1}
}
% define the highlight color, which is typically used for section titles and emphasized text
% You can call this in the middle of the poster, typically before a section
\newcommand{\sethighlightcolor}[1]{
\gdef\highlightcolor{#1}
}
% define the poster colors from the main color
% The main color becomes the highlight color
% The variables defined here can be redefined anywhere in the poster
\newcommand{\postersettings}[1]{
\sethighlightcolor{#1}
\gdef\emphcolor{\highlightcolor}
\gdef\bannercolor{\highlightcolor}
\gdef\titlecolor{white}
\gdef\subtitlecolor{gray}
\gdef\footercolor{\highlightcolor}
\gdef\sectioncolor{\highlightcolor}
\gdef\subsectioncolor{gray}
\gdef\paragraphcolor{gray}
\gdef\boxcolor{lriyellow}
}
% the four main settings for the color and banner image
\newcommand{\redposter}{
\postersettings{lrired}
\posterbanner{redbanner.jpg}
}
\newcommand{\greenposter}{
\postersettings{lrigreen}
\posterbanner{greenbanner.jpg}
}
\newcommand{\blueposter}{
\postersettings{lriblue}
\posterbanner{bluebanner.jpg}
}
\newcommand{\yellowposter}{
\postersettings{lrigold}
\posterbanner{yellowbanner.jpg}
}
% default to red poster
\redposter
%========== \makeposter macro ========================================
% the commands that can be used before \makeposter
\newcommand{\posterlang}[1]{\gdef\Poster@Lang{-#1}}
% one of \redposter, \greenposter or \blueposter should be used
% \title can be used (it's already defined by LaTeX)
\newcommand{\titleright}[1]{\gdef\Poster@TitleRight{#1}}
\renewcommand{\subtitle}[1]{\subtitletrue\gdef\Poster@Subtitle{#1}}
\newcommand{\subtitleright}[1]{\subtitletrue\gdef\Poster@SubtitleRight{#1}}
\newcommand{\group}[1]{\gdef\Poster@Group{#1}}
\newcommand{\inrialogo}{\inrialogotrue}
\newcommand{\titleLR}[2]{\title{#1}\titleright{#2}}
\newcommand{\subtitleLR}[2]{\subtitle{#1}\subtitleright{#2}}
% inner commands to manage \makeposter
\newif\ifinrialogo
\newif\ifsubtitle
\def\Poster@Lang{}
\def\Poster@Group{\hspace*{1cm}}
\def\Poster@TitleRight{}
\def\Poster@SubtitleRight{}
% the \makeposter macro to output the header and footer
\newcommand{\makeposter}{
\setlength{\unitlength}{1cm}
\begin{picture}(0,0)
% top banner + title and subtitle if any
\put(-0.5,-3){\includegraphics[width=\bannerwidth,height=3.5cm]{\Poster@Banner}}
\put(-0,-3){\includegraphics[width=3cm]{\Poster@ImageDir/logoLRI.pdf}}
\put(-0.5,-4.7){\color{\bannercolor}\rule{\bannerwidth}{1.7cm}}
\put(0,-4.05){\parbox[l]{\bannerwidth}{\textcolor{\titlecolor}{\Huge\textsf\@title}}}
\put(-1,-4.05){\parbox[c]{\bannerwidth}{\begin{flushright}\textcolor{\titlecolor}{\Large\textsf\Poster@TitleRight}\end{flushright}}}
\put(0,-5.4){\ifsubtitle\parbox[c]{\bannerwidth}{\textcolor{\subtitlecolor}{\Large\textsf\Poster@Subtitle}}\fi}
\put(-1,-5.4){\ifsubtitle\parbox[c]{\bannerwidth}{\begin{flushright}\textcolor{\subtitlecolor}{\Large\textsf\Poster@SubtitleRight}\end{flushright}}\fi}
% footer: line with logos underneath and the "i"+group name at the bottomright
\put(-0.5,-39){\color{\footercolor}\rule{\bannerwidth}{.25cm}}
\put(-0.5,-39.6){\parbox[c]{\bannerwidth}{\begin{flushright}
\includegraphics[height=0.05\textwidth]{\Poster@ImageDir/logoUPS.pdf}
\hfill\includegraphics[height=0.05\textwidth]{\Poster@ImageDir/logoCNRS\Poster@Lang.pdf}
\ifinrialogo\hfill\includegraphics[height=0.05\textwidth]{\Poster@ImageDir/logoINRIA\Poster@Lang.pdf}\fi
\hfill\includegraphics[height=0.07\textwidth]{\Poster@ImageDir/i.pdf}\hspace{-2mm}%
\raisebox{2mm}{\textsf{\Large{\Poster@Group}}}\end{flushright}}
}
\end{picture}
\ifsubtitle\vspace*{5.6cm}\else\vspace*{4.6cm}\fi
}
%========== Chapter and Section titles ========================================
\usepackage{titlesec}
% specify whether section titles are displayed with a line underneath them (defaults to true)
% you can call \titleruletrue and \titlerulefalse anywhere and it will affect all subsequent section titles
\newif\iftitlerule
\titleruletrue
% define the format of section titles: colored text, no numbering, with a rule below if titlerule is true
\titleformat{\section}{\normalfont\LARGE\sffamily\bfseries\color{\sectioncolor}}{}{0pt}{}%
[\iftitlerule{\color{\sectioncolor}\titlerule[2pt]\vspace{-7pt}}\fi]
% define the format of subsection titles: colored text, no numbering
\titleformat{\subsection}{\normalfont\Large\sffamily\bfseries\color{\subsectioncolor}}{}{0pt}{}
% define the format of paragraph titles: colored text, inline with the rest of the paragraph
\titleformat{\paragraph}[runin]{\normalfont\large\sffamily\bfseries\color{\paragraphcolor}}{}{1em}{}
%========== Multi columns layout ========================================
% the separation between columns for the 2- and 3-column layouts - these can be changed
\newlength\twocolsep\setlength\twocolsep{1.5cm}
\newlength\threecolsep\setlength\threecolsep{1cm}
% the width of the text in one, two and three columns - don't change these!
\newlength\onecolwidth\setlength\onecolwidth{\textwidth}
\newlength\twocolwidth\setlength\twocolwidth{(\textwidth - \twocolsep)/2}
\newlength\threecolwidth\setlength\threecolwidth{(\textwidth - 2\threecolsep)/3}
% the current width of the text - don't change this!
\newlength\colwidth\setlength\colwidth{\onecolwidth}
% To format a section in two-columns, do this (the title spans the two columns):
% \twocolsection{<sectiontitle}
% text .. text ..
% \columnbreak % force a column break (if needed)
% text .. text ..
% \onecol
%
% To format text (without a title) in two-columns, do this:
% \twocoltext
% text .. text ..
% \columnbreak % force a column break (if needed)
% text .. text ..
% \onecol
%
% Three-column format is achieved similarly with
% \threecolsection{<sectiontitle>} ... \onecol
% \threecoltext ... \onecol
% This can be used to have two columns of text and an in the third column.
% start a section with 2-column format
% the argument is the title of the section
\newcommand{\twocolsection}[1]{
\setlength\columnsep{\twocolsep}\setlength\colwidth{\twocolwidth}
\begin{multicols}{2}[\section{#1}]
\raggedcolumns
}
% start 2-column text
\newcommand{\twocoltext}{
\setlength\columnsep{\twocolsep}\setlength\colwidth{\twocolwidth}
\begin{multicols}{2}
\raggedcolumns
}
% start a section with 3-column format
% the argument is the title of the section
\newcommand{\threecolsection}[1]{
\setlength\columnsep{\threecolsep}\setlength\colwidth{\threecolwidth}
\begin{multicols}{3}[\section{#1}]
\raggedcolumns
}
% start 3-column text
\newcommand{\threecoltext}{
\setlength\columnsep{\threecolsep}\setlength\colwidth{\threecolwidth}
\begin{multicols}{3}
\raggedcolumns
}
% end of 2- or 3-column section or text
\newcommand{\onecol}[1]{
\end{multicols}
\setlength\colwidth{\onecolwidth}
}
%========== Boxes ========================================
% The size of the margin around the text when it is put inside a colored box - can be changed
\newlength\coloredboxmargin\setlength\coloredboxmargin{0.4cm}
% The width of the text inside the coloredbox
\newlength\coloredboxwidth
% To format text on a colored background:
% \begin{coloredbox}{<colorname>}
% ... text ...
% \end{coloredbox}
%
% Note that in multicolumn layout, you can only put text in colored box within a column,
% i.e. you cannot have a coloredbox environment around a \twocoltext ... \onecol block.
% (If someone knows how to fix this let me know!)
%
\newenvironment{coloredbox}[1]%
{\setlength\coloredboxwidth{\colwidth - 2\coloredboxmargin}%
\def\Box@color{#1}\setlength{\fboxsep}{\coloredboxmargin}\begin{Sbox}\begin{minipage}{%
\coloredboxwidth}\setlength{\parskip}{2ex}\vspace{-\parskip}}%
{\end{minipage}\end{Sbox}\colorbox{\Box@color}{\TheSbox}}
% A shortcut for a gray background:
% \begin{graybox}
% ...
% \end{graybox}
%
\newenvironment{graybox}%
{\begin{coloredbox}{lightgray}}%
{\end{coloredbox}}
% A shortcut for a background:
% \begin{cbox}
% ...
% \end{cbox}
%
\newenvironment{cbox}%
{\begin{coloredbox}{\boxcolor}}%
{\end{coloredbox}}

10
scripts/build.sh Executable file
View File

@ -0,0 +1,10 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../
xelatex -shell-escape src/poster-jdse-2017.tex
xelatex -shell-escape src/poster-jdse-2017.tex
xelatex -shell-escape src/poster-jdse-2017.tex
)

9
scripts/clean.sh Executable file
View File

@ -0,0 +1,9 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../
rm -f ./*.log ./*.tuc ./*.out ./*.aux ./*.toc ./*.pyg
)

9
scripts/mrproper.sh Executable file
View File

@ -0,0 +1,9 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../
rm -f ./*.pdf
)

15
scripts/test.sh Executable file
View File

@ -0,0 +1,15 @@
#!/usr/bin/env sh
set -eu
(
cd "$(dirname "$0")"/../
# Testing scripts
# shellcheck disable=SC2185
find -O3 . -type f -name '*.sh' -exec shellcheck {} \;
# shellcheck disable=SC2185
find -O3 . -type f -name '*.tex' -exec chktex -q --nowarn 26 --nowarn 15 --nowarn 17 {} \;
## shellcheck disable=SC2185
# find -O3 . -type f -name '*.tex' -exec lacheck {} \; # TODO: fix lacheck so it's possible to disable some warnings which are incorrects...
)

43
src/packages.tex Normal file
View File

@ -0,0 +1,43 @@
% Specify the input encoding (uncomment one of the 2 lines below)
\usepackage[utf8]{inputenc}
%\usepackage{isolatin1}
% [optional] Edit the line below with the path (absolute or relative) to the template directory
\def\templatedir{.}
% Include the LRI poster package
\usepackage{\templatedir/includes/poster}
%========================================
% The header and footer of the poster
%========================================
% Uncomment the line below to use the French or English version of the CNRS and Inria logos.
% If both lines are commented out, the CNRS logo without the tag line is used, and the English version of the Inria logo is used.
%\posterlang{fr}
\posterlang{en}
% Select the poster color.
% \redposter for group posters
% \blueposter for doctoral student posters
% \greenposter for project posters
%\redposter
%\blueposter
%\greenposter
\yellowposter{}
% [optional] Set the name of the group (displayed to the right of the "i" at the bottom right corner of the poster)
\group{www.lri.fr}
% Uncomment the lines below if you want the INRIA logo in addition to the Paris-Sud and CNRS logos
\inrialogo{}
% xcolor
\definecolor{darkBackground}{HTML}{282c34} % source code background
\definecolor{darkBackgroundHighlight}{HTML}{2c323c} % source code background
\definecolor{lightBackground}{HTML}{D7D3CB} % source code background
% source code
\usepackage[cache=false, draft=false]{minted}
\usemintedstyle{paraiso-dark}
\setminted{bgcolor=lightBackground}
\setminted{linenos, autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{9pt}{7pt}, frame=none, stepnumber=2}

193
src/poster-jdse-2017.tex Normal file
View File

@ -0,0 +1,193 @@
%========================================
% LRI Poster
%========================================
% To format: use pdflatex
%
% The resulting PDF file is in A3.
% To print as a poster, use the printer driver settings to enlarge to the target size
%
%----------------------------------------
\documentclass[12pt]{scrartcl}
\input{src/packages.tex}
\begin{document}
\input{src/title.tex}
% Generate the poster header and footer
\makeposter{}
%----------------------------------------
\section{Data and proofs}
%----------------------------------------
Data is everywhere etc. Proofs and formal methods not often applied to data languages (SQL) or DBMS (postgresql) etc.
%Le poster est formatté avec LaTeX. Les instructions détaillées sont dans le fichier source et le source de ce poster peut servir d'exemple.
%Le texte peut être formatté en une, deux ou trois colonnes. Ceci est un exemple de texte formatté sur une colonne. Compte tenu de la largeur du poster, il est préférable de limiter ce texte à quelques lignes.
%----------------------------------------
\vspace{1cm}% add space for better visual balance
\twocoltext{}
%----------------------------------------
\section{Certified parsing, from SQL to SQLCoq}
\inputminted[bgcolor=darkBackground]
{sql}
{src/query_14.sql}
We parse SQL queries using the certified parser generator written by Jacques-Henri Jourdan and used in CompCert. At the end, we have an SQLCoq-compatible representation of the query. SQLCoq is a Coq library formalising SQL.
%Pour formatter le texte sur \emph{deux colonnes}, utiliser la macro \verb|\twocolsection{<titre>}| si vous souhaitez un titre de section qui fasse la largeur du poster, ou bien \verb|\twocoltext| pour ne pas afficher de titre.
%Vous pouvez utiliser les commandes habituelles à l'intérieur d'une colonne~:
%\begin{itemize}
% \item \verb|\section{<titre>}|,
% \item \verb|\subsection{<titre>}|,
% \item \verb|\paragraph{<titre>}|.
%\end{itemize}
%Pour changer de colonne, utiliser la commande \verb|\columnbreak| et à la fin de la deuxième columne, utiliser la commande \verb|\onecol|.
\columnbreak{}
%........................................
\section{Involving DBMS, from SQL to unified execution plan}
We give an SQL query to two DBMS (PostgreSQL and Oracle) and get the query execution plan, that is, the algorithms which are going to be used to fetch the data from the disk.
Then, we change the plans so they have the same format. We defined an unified execution plan format.
%Les titres de sections sont formattés dans la couleur du thème du poster.
%le trait sous le titre peut être désactivé / réactivé avec les commandes \verb|\titlerulefalse| et \verb|\titleruletrue|.
%\subsection{Sous-sections}
%Les titres de sous-sections sont formattés en gris.
%\paragraph{Paragraphes}
%Les titres de paragraphes sont aussi formattés en gris, mais sont inclus dans le paragraphe.
%Pour mettre du texte \emph{en évidence}, utiliser la commande habituelle \verb|\emph{...}|.
\onecol{}
%----------------------------------------
\threecolsection{From unified plan to Extended Algebra}
%----------------------------------------
\inputminted[bgcolor=lightBackground]
{xml}
{src/query_14.xml}
%Pour formatter le texte sur \emph{trois colonnes}, c'est le même principe que pour deux colonnes mais avec les commandes \verb|\threecolsection{<titre>}| et \verb|\threecoltext|.
%Il faut bien sûr utiliser deux fois la commande \verb|\columnbreak| pour séparer les trois colonnes entre elles, et terminer avec \verb|\onecol|.
\columnbreak{}
%........................................
From a given plan, we build an Extended Algebra expression. ExtAlg is similar to Relationnal Algebra but more powerful.
Here, the expression is annotated with algorithms. Thus, we'll be able to go further by executing the algorithms which were formalized in Coq.
%Vous pouvez insérer des images avec la commande habituelle \verb|\includegraphics|.
%Quel que soit le nombre de colonnes courant, la largeur de la colonne est dans la variable \verb|\colwidth|.
%Pour que l'image fasse la largeur de la colonne, il suffit de d'utiliser l'option \verb|[width=\colwidth]|.
\columnbreak{}
%........................................
%\begin{center}
%\includegraphics[width=0.4\colwidth]{img/logoLRI.pdf}\\
%{\footnotesize\sffamily Le logo du LRI}
%\end{center}
%{\setmonofont{Everson Mono}
\inputminted[bgcolor=darkBackground]
{ocaml}
{src/query_14.extalg}
%}
\onecol{}
%----------------------------------------
\twocolsection{Equivalence of two ExtAlg queries}
%----------------------------------------
Now we have the ExtAlg expression of the query from the plan the DBMS gave us. We also have the SQLCoq representation of the query. We can get the ExtAlg expression from the SQLCoq representation. We can show the equivalence of the two ExtAlg queries, by using normal forms on logical formulas, or using other Coq-proved equivalence on ExtAlg.
%\begin{cbox}
%Pour mettre un paragraphe en évidence, vous pouvez utiliser l'environnement \verb|cbox| qui formatte le texte sur un fond de couleur jaune sable.
%\end{cbox}
%\begin{graybox}
%L'environnement \verb|graybox| fait la même chose avec un fond de couleur gris clair.
%Enfin l'environnement \verb|coloredbox| fait la même chose avec une couleur quelconque, passée en paramètre.
%\end{graybox}
\columnbreak{}
%........................................
With the equivalence of the two expressions, we are sure that the algorithms that the DMBS planned to use are corrects and that they won't change the semantic of the SQL query. We still have to prove that algorithms used in DBMS are correct, or to use our own written in Coq.
%Il existe trois thèmes de poster : \verb|\redposter|, \verb|\blueposter| et \verb|\greenposter|. La couleur du thème est dans la variable %\verb|\highlightcolor|. Les autres couleurs prédéfinies sont :
%\begin{itemize}
% \item les couleurs des thèmes : \verb|lrired|, \verb|lrigreen|, \verb|lriblue|~;
% \item les couleurs du logo du LRI : \verb|lrilogored|, \verb|lrilogogreen|, \verb|lrilogoyellow|, \verb|lrilogogray|~;
% \item \verb|lriyellow| utilisé pour les boîtes \verb|cbox|, \verb|gray| pour les titres de sous-sections et de paragraphes, et \verb|lightgray| pour les boîtes \verb|graybox|.
%\end{itemize}
\columnbreak{}
%........................................
\onecol{}
\end{document}
%========== Sectioning ========================================
%
% \section, \subsection and \paragraph are supported
%
% Section titles have a line underneath.
% You can remove it by calling \titlerulfalse before a section title,
% and re-enable it by calling \titleruletrue.
%========== Graphics ========================================
%
% Simply use \includegraphics to include PDF files.
% It is best to specify the width of the included graphics as
% a fraction of either \textwidth, the total width of the text area
% or of \colwidth, the width of the current column,
% e.g. \includegraphics[width=0.8\textwidth]{<file>.pdf}
%========== Multi columns layout ========================================
%
% To format a section in two-columns, do this (the title spans the two columns):
% \twocolsection{<sectiontitle}
% text .. text ..
% \columnbreak % force a column break (if needed)
% text .. text ..
% \onecol
%
% To format text (without a title) in two-columns, do this:
% \twocoltext
% text .. text ..
% \columnbreak % force a column break (if needed)
% text .. text ..
% \onecol
%
% Three-column format is achieved similarly with
% \threecolsection{<sectiontitle>} ... \onecol
% \threecoltext ... \onecol
% This can be used to have two columns of text and an in the third column.
%========== Colored boxes ========================================
%
% To format text on a colored background:
% \begin{coloredbox}{<colorname>}
% ... text ...
% \end{coloredbox}
%
% Note that in multicolumn layout, you can only put text in colored box within a column,
% i.e. you cannot have a coloredbox environment around a \twocoltext ... \onecol block.
%
% There are two shortcuts for colored boxes:
% \begin{cbox} ... \end{cbox} a box of the default highlighting color (defined by the poster type)
% \begin{graybox} ... \end{graybox} a gray box

15
src/query_14.extalg Normal file
View File

@ -0,0 +1,15 @@
⍵ {
_ Fine
_ r.dday → r.dday, r.bid → r.bid, r.sid → r.sid, s.age → s.age, s.rating → s.rating, s.sname → s.sname, s.sid → s.sid
_ x_0.s.sid = x_0.r.sid
_ {
⍵ {
_ Fine
_ sid → s.sid, sname → s.sname, rating → s.rating, age → s.age
_
_ {
Seq Scan on sailors
}
}
× (DependentJoin) (Hash Join)
...

1
src/query_14.sql Normal file
View File

@ -0,0 +1 @@
SELECT s.sname FROM sailors s WHERE EXISTS (SELECT * FROM reserves r WHERE r.bid = 103 AND s.sid = r.sid);

12
src/query_14.xml Normal file
View File

@ -0,0 +1,12 @@
<Plan>
<Node-Type>Hash Join</Node-Type>
<Join-Type>Inner</Join-Type>
<Hash-Cond>(s.sid = r.sid)</Hash-Cond>
<Plans>
<Plan>
<Node-Type>Seq Scan</Node-Type>
<Parent-Relationship>Outer</Parent-Relationship>
<Relation-Name>sailors</Relation-Name>
<Alias>s</Alias>
</Plan>
...

13
src/title.tex Normal file
View File

@ -0,0 +1,13 @@
% Set the title (displayed in the rectangle below the banner)
\title{Deep specification and verification of SQL compilation chain }
%\titleright{V1.1}
% alternatively, you can use:
% \titleLR{Comment faire un poster}{V1.0}
\author{Léo Andrès \& Raphaël Cornet \& Eunice Martins}
% [optional] Set the subtitle or the author name (displayed under the title)
\subtitle{Junior Conference on Data Science and Engineering}
\subtitleright{September 2017}
% alternatively, you can use:
% \subtitleLR{pour la visite de l'AERES}{jan 2009}