zapashcanon
2 years ago
commit
3e1f1e22c8
16 changed files with 422 additions and 0 deletions
@ -0,0 +1,14 @@ |
|||
*.pdf |
|||
*.bbl |
|||
*.bcf |
|||
*.blg |
|||
*.log |
|||
*.run.xml |
|||
*.aux |
|||
*.out |
|||
*.cmi |
|||
*.cmx |
|||
*.toc |
|||
*.o |
|||
src/svg-inkscape/ |
|||
*.dot.svg |
|||
|
After Width: | Height: | Size: 5.2 KiB |
@ -0,0 +1,14 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( cd "$(dirname "$0")"/../src |
|||
|
|||
c="texfot xelatex -shell-escape -halt-on-error" |
|||
|
|||
$c main.tex | sed '/Output written/d' | sed '/Rerun to get \/Page/d' | sed '/Warning: Citation/d' | sed '/Warning: Empty bib/d' | sed '/has changed/d' | sed '/Warning: There were/d' | sed '/biblatex Warning/d' |
|||
biber -quiet main |
|||
$c main.tex | sed '/Output written/d' | sed '/Warning: There were/d' | sed '/biblatex Warning/d' |
|||
$c main.tex |
|||
mv main.pdf ../main.pdf |
|||
) | sed '/This is/d' | sed '/texfot: invoking/d' |
|||
@ -0,0 +1,10 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( cd "$(dirname "$0")"/../src/ |
|||
|
|||
rm -f ./*.log ./*.tuc ./*.out ./*.aux ./*.toc ./*.pyg ./*.bbl ./*.bcf ./*.blg ./*.run.xml |
|||
rm -rf ./svg-inkscape/ |
|||
|
|||
) |
|||
@ -0,0 +1,9 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( cd "$(dirname "$0")"/../ |
|||
|
|||
rm -f ./*.pdf |
|||
|
|||
) |
|||
@ -0,0 +1,16 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( |
|||
cd "$(dirname "$0")"/../ |
|||
|
|||
# Testing scripts |
|||
# shellcheck disable=SC2185 |
|||
find -O3 . -type f -name '*.sh' -exec shellcheck {} \; |
|||
cd src/ |
|||
# 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... |
|||
) |
|||
@ -0,0 +1,3 @@ |
|||
\begin{abstract} |
|||
Ce document est un rapport de mon stage sur le sujet \emph{TODO}, effectué dans le cadre de ma formation en Master 2 \bsc{fiil} à l'Université Paris-Saclay. J'y présente TODO. J'ai été encadré par \href{https://dblp.org/pers/c/Chambart:Pierre.html}{Pierre \bsc{Chambart}}. |
|||
\end{abstract} |
|||
@ -0,0 +1,3 @@ |
|||
\section{Answer} |
|||
|
|||
Blablabla |
|||
@ -0,0 +1,5 @@ |
|||
\section{Annexes} |
|||
|
|||
\subsection{Type et exemple d'invariant}\label{type_invariant} |
|||
|
|||
\inputminted[bgcolor=darkBackground]{ocaml}{algo1_part.mlw} |
|||
@ -0,0 +1,150 @@ |
|||
@ARTICLE{Milner78, |
|||
author = {Robin Milner}, |
|||
title = {A theory of type polymorphism in programming}, |
|||
journal = {Journal of Computer and System Sciences}, |
|||
year = {1978}, |
|||
volume = {17}, |
|||
pages = {348--375} |
|||
} |
|||
|
|||
@phdthesis{Filliatre11, |
|||
author = {Jean-Christophe Filli\^atre}, |
|||
title = {Deductive Program Verification}, |
|||
year = 2011, |
|||
month = dec, |
|||
type = {Th\`{e}se d'habilitation}, |
|||
school = {Universit{\'e} Paris-Sud}, |
|||
type_publi = {these}, |
|||
url = {http://www.lri.fr/~filliatr/hdr/memoire.pdf}, |
|||
x-equipes = {demons PROVAL}, |
|||
x-type = {habilitation}, |
|||
x-support = {rapport}, |
|||
topics = {team, proval} |
|||
} |
|||
|
|||
@inproceedings{Filliatre13, |
|||
author = {Jean-Christophe Filli\^atre and Andrei Paskevich}, |
|||
title = {Why3 --- Where Programs Meet Provers}, |
|||
booktitle = {Proceedings of the 22nd European Symposium on Programming}, |
|||
month = mar, |
|||
year = 2013, |
|||
volume = {7792}, |
|||
series = {Lecture Notes in Computer Science}, |
|||
publisher = {Springer}, |
|||
editor = {Matthias Felleisen and Philippa Gardner}, |
|||
pages = {125--128}, |
|||
hal = {http://hal.inria.fr/hal-00789533}, |
|||
topics = {team,lri}, |
|||
keywords = {Why3}, |
|||
type_publi = {icolcomlec}, |
|||
x-equipes = {demons PROVAL}, |
|||
x-type = {article}, |
|||
x-support = {actes}, |
|||
x-cle-support = {ESOP}, |
|||
x-editorial-board = {yes}, |
|||
x-international-audience = {yes} |
|||
} |
|||
|
|||
@inproceedings{Clochard15, |
|||
hal = {http://hal.inria.fr/hal-01162661}, |
|||
author = {Martin Clochard and Jean-Christophe |
|||
Filli\^atre and Andrei Paskevich}, |
|||
title = {How to avoid proving the absence of integer overflows}, |
|||
pages = {94--109}, |
|||
crossref = {vstte15}, |
|||
topics = {team,lri}, |
|||
keywords = {Why3}, |
|||
type_publi = {icolcomlec}, |
|||
x-international-audience = {yes}, |
|||
x-proceedings = {yes} |
|||
} |
|||
|
|||
@techreport{Gondelman16, |
|||
topics = {team}, |
|||
author = {Jean-Christophe Filli\^atre and L\'eon |
|||
Gondelman and Andrei Paskevich}, |
|||
title = {A Pragmatic Type System for Deductive Verification}, |
|||
type = {Research Report}, |
|||
institution = {Universit\'e Paris Sud}, |
|||
year = 2016, |
|||
abstract = { In the context of deductive verication, it is customary |
|||
today to handle programs with pointers using either |
|||
separation logic, dynamic frames, or explicit memory |
|||
models. Yet we can observe that in numerous |
|||
programs, a large amount of code is within the scope |
|||
of Hoare logic, provided we can statically control |
|||
aliasing. When this is the case, the code |
|||
correctness can be reduced to simpler verication |
|||
conditions which do not require any explicit memory |
|||
model. This makes verication conditions more |
|||
amenable both to automated theorem proving and to |
|||
manual inspection and debugging. In this paper, we |
|||
devise a method of such static aliasing control for |
|||
a programming language featuring nested data |
|||
structures with mutable components. Our solution is |
|||
based on a type system with singleton regions and |
|||
eects, which we prove to be sound.}, |
|||
hal = {https://hal.archives-ouvertes.fr/hal-01256434v3}, |
|||
note = {\url{https://hal.archives-ouvertes.fr/hal-01256434v3}} |
|||
} |
|||
|
|||
@article{Gondelman16_2, |
|||
author = {Jean-Christophe Filli\^atre and L\'eon |
|||
Gondelman and Andrei Paskevich}, |
|||
title = {The Spirit of Ghost Code}, |
|||
journal = {Formal Methods in System Design}, |
|||
publisher = {Springer}, |
|||
year = 2016, |
|||
volume = 48, |
|||
number = 3, |
|||
pages = {152--174}, |
|||
issn = {1572-8102}, |
|||
doi = {10.1007/s10703-016-0243-x}, |
|||
topics = {team}, |
|||
hal = {https://hal.archives-ouvertes.fr/hal-01396864v1}, |
|||
keywords = {Why3}, |
|||
type_publi = {irevcomlec}, |
|||
x-international-audience = {yes}, |
|||
x-proceedings = {yes}, |
|||
x-type = {article}, |
|||
x-support = {revue}, |
|||
x-editorial-board = {yes}, |
|||
abstract = { |
|||
In the context of deductive program verification, ghost code is part |
|||
of the program that is added for the purpose of specification. |
|||
Ghost code must not interfere with regular code, in the sense that |
|||
it can be erased without observable difference in the program outcome. |
|||
In particular, ghost data cannot participate in regular |
|||
computations and ghost code cannot mutate regular data or diverge. |
|||
The idea exists in the folklore since the early notion of auxiliary |
|||
variables and is implemented in many state-of-the-art program |
|||
verification tools. However, a rigorous definition and treatment of |
|||
ghost code is surprisingly subtle and few formalizations exist. |
|||
|
|||
In this article, we describe a simple ML-style programming language |
|||
with mutable state and ghost code. Non-interference is ensured by a |
|||
type system with effects, which allows, notably, the same data types |
|||
and functions to be used in both regular and ghost code. |
|||
We define the procedure of ghost code erasure and we prove its |
|||
safety using bisimulation. |
|||
A similar type system, with numerous extensions which we briefly discuss, |
|||
is implemented in the program verification environment Why3. |
|||
} |
|||
} |
|||
|
|||
@techreport{Filliatre18, |
|||
author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and |
|||
Andrei Paskevich and M{\'a}rio Pereira and Sim{\~a}o Melo de Sousa}, |
|||
title = {A Toolchain to {P}roduce {C}orrect-by-{C}onstruction {OC}aml |
|||
{P}rograms}, |
|||
hal = {https://hal.inria.fr/hal-01783851}, |
|||
pdf = {https://hal.inria.fr/hal-01783851/file/main.pdf}, |
|||
note = {artifact: \url{https://www.lri.fr/~mpereira/correct_ocaml.ova}}, |
|||
year = {2018} |
|||
} |
|||
|
|||
@misc{AlgoPS, |
|||
title = {Document de présentation des algorithmes de Parcoursup}, |
|||
year = 2019, |
|||
url = {https://framagit.org/parcoursup/algorithmes-de-parcoursup/blob/master/doc/presentation_algorithmes_parcoursup_2019.pdf} |
|||
} |
|||
@ -0,0 +1 @@ |
|||
\section{Conclusion} |
|||
@ -0,0 +1,28 @@ |
|||
\documentclass[a4paper,12pt,titlepage]{extarticle} |
|||
|
|||
\input{packages.tex} |
|||
|
|||
\bibliography{bib} |
|||
|
|||
\begin{document} |
|||
|
|||
\input{title.tex} |
|||
|
|||
\input{abstract.tex} |
|||
|
|||
\tableofcontents |
|||
|
|||
\newpage{} |
|||
|
|||
\input{ocp.tex} |
|||
\input{problem.tex} |
|||
\input{answer.tex} |
|||
\input{conclusion.tex} |
|||
|
|||
\appendix |
|||
|
|||
%\input{appendix.tex} |
|||
|
|||
\printbibliography{} |
|||
|
|||
\end{document} |
|||
@ -0,0 +1,3 @@ |
|||
\section{OCamlPro} |
|||
|
|||
Blablabla |
|||
@ -0,0 +1,67 @@ |
|||
\usepackage[french]{babel} |
|||
|
|||
\usepackage{euler} |
|||
\usepackage{fontspec} % encoding |
|||
|
|||
\usepackage{graphicx} % to include img |
|||
\usepackage{enumitem} % powerful lists |
|||
\usepackage{xspace} % correct quotes printing |
|||
\usepackage[np]{numprint} % correct numbers printing |
|||
\usepackage{amsmath} % maths and better typo |
|||
\usepackage{amssymb} % more maths |
|||
\usepackage{dsfont} % and even more maths |
|||
\usepackage{color} % color power |
|||
\usepackage[dvipsnames, table]{xcolor} % more color power |
|||
\usepackage{microtype} % better typo |
|||
|
|||
\usepackage{hyperref} % internal and external links (e.g. mail, www) |
|||
\usepackage{cleveref} |
|||
|
|||
\usepackage[cache=false, draft=false]{minted} % source code |
|||
|
|||
\usepackage{placeins} % float displaying |
|||
\usepackage{csquotes} |
|||
\usepackage{ellipsis} % correct ... |
|||
\usepackage[notransparent]{svg} |
|||
|
|||
\usepackage[ |
|||
autolang=other, |
|||
backend=biber, % choix de l'outil de traitement |
|||
backref=true, % liens dans la bibliographie pour remonter dans le texte |
|||
backrefstyle=none, % afficher toutes les utilisations de la référence |
|||
bibstyle=alphabetic, % style pour les clés des références dans la bibliographie : [initialesAnnée] |
|||
citestyle=alphabetic, % style pour les clés des références dans le texte : [initialesAnnée] |
|||
sorting=none, % bibliographie triée par ordre d'utilisation des références |
|||
]{biblatex} % support des bibliographies |
|||
|
|||
\usepackage{calligra} |
|||
\usepackage[bottom]{footmisc} |
|||
\usepackage{wrapfig} |
|||
|
|||
\setmainfont{Linux Libertine O} |
|||
\setsansfont{Linux Biolinum O} |
|||
%\setmonofont{Source Code Pro} |
|||
%\newfontfamily\unicodemonofont{Everson Mono} |
|||
|
|||
\newcommand\myshade{85} |
|||
\colorlet{mylinkcolor}{violet} |
|||
\colorlet{mycitecolor}{YellowOrange} |
|||
\colorlet{myurlcolor}{Aquamarine} |
|||
|
|||
\usemintedstyle{paraiso-dark} |
|||
\setminted{bgcolor=lightBackground} |
|||
\setminted{linenos, autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{12pt}{12pt}, frame=none, stepnumber=2} |
|||
|
|||
\hypersetup{linkcolor = mylinkcolor!\myshade!black, |
|||
citecolor = mycitecolor!\myshade!black, |
|||
urlcolor = myurlcolor!\myshade!black, |
|||
colorlinks = true, |
|||
pdfstartview=FitH |
|||
} |
|||
|
|||
\graphicspath{{./../img/}} |
|||
|
|||
\definecolor{darkBackground}{HTML}{282c34} % source code background |
|||
\definecolor{darkBackgroundHighlight}{HTML}{2c323c} % source code background |
|||
\definecolor{lightBackground}{HTML}{D7D3CB} % source code background |
|||
\definecolor{processblue}{cmyk}{0.96,0,0,0} |
|||
@ -0,0 +1 @@ |
|||
\section{Le problème} |
|||
@ -0,0 +1,29 @@ |
|||
\begin{titlepage} |
|||
\begin{center} |
|||
\newcommand\important{\huge \scshape } |
|||
\newcommand\notimportant{\Large} |
|||
\newcommand\vspa[1]{\vspace*{#1\textheight}} |
|||
|
|||
\important{} Dddddml |
|||
|
|||
\vspa{0.1} |
|||
|
|||
\notimportant{} Rapport de stage par\\ |
|||
\important{} Léo \bsc{Andrès}\\ |
|||
\vspa{0.02} |
|||
\notimportant{} 15 septembre 2020\\ |
|||
|
|||
\vspa{0.1} |
|||
|
|||
\notimportant{} Master 2\\ |
|||
Fondements de l'Informatique\\ |
|||
et Ingénierie du Logiciel\\ |
|||
\vspa{0.05} |
|||
\includesvg[width=200pt]{universite-paris-saclay.svg}\\ |
|||
|
|||
\vspa{0.1} |
|||
|
|||
\notimportant{} Sous la direction de\\ |
|||
\important{} Pierre~\bsc{Chambart} |
|||
\end{center} |
|||
\end{titlepage} |
|||
Loading…
Reference in new issue