write stuff

src/abstract.tex

@@ -1,3 +1,6 @@
 \begin{abstract}
-  Ce document est un rapport de mes travaux de recherche sur le sujet \emph{TODO}, effectué dans le cadre de ma formation en Master 1 Informatique à l'Université Paris-Saclay, j'ai été encadré par \href{https://www.lri.fr/~filliatr/}{Jean-Christophe \bsc{Filliâtre}}.
+  % TODO: m1 -> mag2
+  % ingénieur d'étude
+  % ter -> ?
+  Ce document est un rapport de mes travaux de recherche sur le sujet \emph{Vérification par preuve formelle de propriétés fonctionnelles d'algorithmes de classification}, effectué dans le cadre de ma formation en Master 1 Informatique à l'Université Paris-Saclay, j'ai été encadré par \href{https://www.lri.fr/~filliatr/}{Jean-Christophe \bsc{Filliâtre}}.
 \end{abstract}

src/mf.tex

@@ -2,7 +2,7 @@
 
   Le \bsc{lri}\footnote{Laboratoire de Recherche en Informatique.} est un laboratoire de l'Université Paris-Sud. C'est une \bsc{umr}\footnote{Unité Mixte de Recherche.} du \bsc{cnrs}.
 
-  Le \bsc{lri} est composé de plusieurs équipes dont notamment l'équipe \bsc{vals}\footnote{Vérification, Algorithmes, Langages et Systèmes.}. L'équipe \bsc{vals} mène de nombreux travaux dans le domaine des méthodes formelles.
+  Le \bsc{lri} est composé de plusieurs équipes dont notamment l'équipe \bsc{vals}\footnote{Vérification, Algorithmes, Langages et Systèmes.}, qui mène de nombreux travaux dans le domaine des méthodes formelles.
 
   \subsection{\enquote{Software is hard.}}
 

src/preuves.tex

@@ -1,11 +1,20 @@
 \section{Preuves et implém whyml vérifiée avec Why3...}
-
-  \subsection{Typage, terminaison, safety etc.}
-
+  % TODO: implém de réf. en whyml
+  \subsection{Propriétés génériques}
+    Avant toute chose, on souhaite vérifier un ensemble de propriétés que tout programme se doit de respecter.
+  \subsubsection{Typage} % TODO, au début ?
+    % TODO
+    Par construction, notre programme est bien typé, sans quoi il serait rejeté par Why3.
+    % TODO
+    \subsubsection{Terminaison}
+      On dit qu'un programme termine sur une entrée s'il finit par s'arrêter sur cette entrée. On souhaite montrer la terminaison pour l'ensemble des entrées du programme. Seules quelques constructions du langage peuvent produire un programme qui ne termine pas: boucles \texttt{while}, fonctions récursives etc. Lorsque l'on utilise une telle construction, il suffit généralement d'exhiber un terme dont la valeur décroit et de montrer que l'on va finir par s'arrêter. Par exemple, dans la boucle \texttt{while} qui ajoute un candidat à l'ordre d'appel, on répète le corps de la boucle tant que la taille de l'ordre d'appel est strictement inférieure au nombre initial de candidats dans le classement pédagogique. Il suffit de fournir le \emph{variant}:
+      \[\texttt{nb initial de candidats}~-~\texttt{taille de l'ordre d'appel}\]
+pour prouver la terminaison de la boucle.
+      On a montré que l'ensemble du programme termine.
+    \subsubsection{Sûreté}
+      Une autre propriété que l'on souhaite montrer est la sûreté. On veut par exemple montrer que lorsque l'on accède au $i^\texttt{ème}$ élément d'un tableau, $0 \leq i < n$ avec $n$ la taille du tableau. Un tel accès ayant généralement lieu au sein d'une boucle, il suffit de maintenir un invariant sur l'indice auquel on accède et de le prouver.
+      On a montré la sûreté de l'ensemble du programme.
   \subsection{Preuves de P0, P1, ..., P5}
 
-  \subsection{Extraction}
-
-    extraction...
-
-    implém de réf... (vérifier les classements obtenus)
+  \subsection{Production de code exécutable}
+    Il est possible de générer du code dans un autre langage à partir de l'implémentation WhyML, on appelle cela l'\emph{extraction}. On a extrait notre code vers OCaml. En compilant le code OCaml extrait, on obtient ainsi une imlémentation de référence, que l'on peut exécuter avec des données anonymisées et comparer les résultats obtenus.