Ajout d'un gros exemple d'utilisation de l'équivalence.

FinalExample.java

@@ -0,0 +1,103 @@
+///////////////// COMMON TO BOTH CLASS TABLES /////////////////
+class Optional extends Object {}
+class Some extends Optional {
+    Object value;
+    Object orElse(Object e){
+        return this.value;
+    }
+}
+class None extends Optional {
+    Object orElse(Object e){
+        return e;
+    }
+}
+
+class Static extends Object {
+    /*
+        Makes sure that the input list is a "real" one,
+        that is, one created with [] and :: (List and Cons).
+        Cannot reduce to any value if not.
+    */
+    List ensure(List in) {
+        return in.isEmpty().ite((List)in,(Cons)in);
+    }
+}
+
+//////////////// FIRST CLASS TABLE /////////////////
+class MinGetter extends Object {
+    /*
+        Returns the lesser of the two input integers
+    */
+    Int min(Int a, Int b){
+        return a.lt(b).ite(a,b);
+    }
+    /*
+        Returns the minimum of the input list, None if the list is empty.
+    */
+    Optional listMin(List a) {
+        return a.ensureFinite().isEmpty().ite(new None(), new Some(this.min((Int)this.listMin(a.tail).orElse(a.head), a.head)))
+    }
+}
+class Sort extends Object {
+    List sort(List in){
+        ensure(in).isEmpty().ite(in,minOnStart(in,(Int)((Some)new MinGetter().listMin(in)).value));
+    }
+    /*
+        Put the first occurence of 'min' in 'in' to the start of the list and sort the rest.
+    */
+    List minOnStart(List in, Int min) {
+        return min::this.sort(in.removeFirst(min));
+    }
+}
+
+///////////////// SECOND CLASS TABLE /////////////////
+class MaxGetter extends Object {
+    /*
+        Returns the bigger of the two input integers
+    */
+    Int max(Int a, Int b){
+        return a.gt(b).ite(a,b);
+    }
+    /*
+        Returns the maximum of the input list, None if the list is empty
+    */
+    Optional listMax(List a) {
+        return a.ensureFinite().isEmpty().ite(
+            new None(), 
+            new Some(this.max((Int)this.listMax(a.tail).orElse(a.head), (Int)a.head)))
+    }
+}
+
+class Sort extends Object {
+    
+    List sort(List in){
+        return this.sortAcc(in, []);
+    }
+    
+    List sortAcc(List in, List acc) {
+        ensure(in).isEmpty().ite(acc,maxToEnd(in,((Some)new MaxGetter().listMax(in)).value));
+    }
+    
+    /*
+        Removes max from in, applies sortAcc on the new list, and adds max to the accumulator.
+    */
+    List maxToEnd(List in, Int max) {
+        return this.sortAcc(in.removeFirst(max), max::in.removeFirst(max));
+    }
+}
+
+///////////////// TEST INTERFACE /////////////////¨
+// These three lines gives access to Integer construction
+Int ()
+S (Int)
+S <: Int
+
+// These three lines allows line construction
+List ()
+Cons (List, o)
+Cons <: List
+
+// These two lines allows use of the sort function,
+// the only one whose implementation differs between the two class tables.
+Sort ()
+Sort: sort(List)

RapportStage.tex

@@ -614,12 +614,65 @@
 			Ce théorème était en quelque sorte l'objectif de cette redéfinition, puisque nous comparons dorénavant les expressions sur \enquote{toutes les valeurs qu'elles pourraient renvoyer}.
 			
 			La démonstration se fera sur une version plus puissante du théorème où $h$ peut prendre plusieurs trous. La preuve se fait ensuite par récurrence sur la longueur de la chaine de réduction, en discriminant selon l'emplacement de la réduction (dans $h$, dans $e$ ou entre les deux), et en changeant les noms de variables afin de pouvoir boucler la récurrence. La démonstration complète est présentée en \autoref{anx:proofHValCL}.
-		
-		
+			
+			\subsection{Un exemple concret}
+				Je vais enfin présenter un exemple de \eng{class tables} qui sont différentes et qui seront équivalentes sous une certaine \eng{class table} que je donnerai également.
+				
+				Ces \eng{class table} auront pour objectif de définir une fonction de trie de listes (\fj{Sort.sort}), en utilisant deux algorithmes récursif différents. Le premier qui trouve le minimum de la liste, le place au début de cette dernière puis trie le reste. Le second trouve le maximum de la liste, le place à la fin (à l'aide d'un accumulateur), puis trie le reste.
+				
+				Nous utiliserons quatre classes communes aux deux class tables présentées \autoref{fig:equivex:common} Les trois premières définirons la classe \fj{Optional} qui fonctionne comme \lstinline[language=Caml]|a' option| en OCaml, et qui peut contenir une valeur ou non. Nous définirons aussi une méthode \fj{ensure(List in)} qui nous permet de nous assurer que nous n'avons pas créé de nouvelles classes se substituant aux constructeurs privilégiés des listes (\fj{[]} et \fj{::}).
+				
+				La première classe table \autoref{fig:equivex:first} et la seconde classe table \autoref{fig:equivex:second} définissent toutes deux une première classe d'utilité afin de calculer des minimums/maximums. Les seconde classes sont celles qui font le processus de tri à proprement parler.
+				
+				Enfin, la \eng{test interface} présentée \autoref{fig:equivex:ti} est assez restreinte afin d'éviter de trop discriminer nos deux classes.
+				
+				\begin{figure}
+					\begin{tcolorbox}
+						\small
+						\lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={2-24}]{FinalExample.java}
+					\end{tcolorbox}
+					\caption{Classes communes aux deux \eng{class tables}}
+					\label{fig:equivex:common}
+				\end{figure}
+				\begin{figure}
+					\begin{tcolorbox}
+						\small
+						\lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={27-51}]{FinalExample.java}
+					\end{tcolorbox}
+					\caption{Première \eng{class tables}}
+					\label{fig:equivex:first}
+				\end{figure}
+				\begin{figure}
+					\begin{tcolorbox}
+						\small
+						\lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={54-87}]{FinalExample.java}
+					\end{tcolorbox}
+					\caption{Seconde \eng{class tables}}
+					\label{fig:equivex:second}
+				\end{figure}
+				\begin{figure}
+					\begin{tcolorbox}
+						\small
+						\lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={90-103}]{FinalExample.java}
+					\end{tcolorbox}
+					\caption{La \eng{test interface} utilisée pour la compairaison}
+					\label{fig:equivex:ti}
+				\end{figure}
+			
+				Je ne vais pas présenter ici une preuve formelle de l'équivalence de ces deux classes, notamment parce que c'est assez compliqué sans d'autres théorèmes, la définition étant sémantique, il nous manquerai un théorème qui permettrai de se ramener, par exemple, à l'évaluation de chaque méthode. J'ai quelque peu essayé de construire certains de ces théorèmes, mais je n'ai pas eu le temps d'en obtenir un utile avant la fin de mon stage (même si le \eng{context lemma} fournit un très bon moyen de prouver de tels théorèmes).
+				
+				Algorithmiquement, nous pouvons nous convaincre que les méthodes font ce qui leur est demandé, et l'équivalence algorithmique des deux façons de faire est assez simple.
+				
+				Cet exemple nous fournit néanmoins quelques remarques supplémentaires. Nous pouvons remarquer que certaines constructions out dû être utilisées afin de prévenir d'un utilisateur qui puisse intercaler des classes différentes altérant le fonctionnement de notre programme, notamment pour la classe \fj{List} qui est utilisable par le programme de test. Une solution qui pourrait être envisagée (et d'ailleurs celle retenue dans le Java officiel) est l'ajout d'un mot-clé \fj{final} sur les noms de classes des \eng{test interfaces} qui empêcherai aux classes d'une \eng{class table} l'implémentant d'étendre d'une classe marquée \eng{final}, au delà des extensions indiquées.
+				
+				
+			
 	\section{Conclusion}
 		
 		Nous avons donc créé un préordre en définissant une nouvelle structure de \eng{test interface}. Cette structure est à la fois assez puissante pour que l'on puisse tester profondément les programmes, mais aussi assez tolérante pour que l'équivalence ne s'arrête pas sur la moindre différence de grammaire. Nous avons aussi obtenu un \eng{context lemma} pour notre préordre, ce qui nous conforte dans son bon fondement.
 		
+		Nous pourrions complexifier la structure en observant d'autres problèmes, par exemple, la comparaison des valeurs de retour (finies ou infinies) n'a pas de limitation sur les types des objets. Nous pourrions imaginer une libraire dont on aimerai qu'elle renvoie un objet \fj{State} décrivant son état, que la \eng{test interface} n'autorise pas à utiliser, si ce n'est comme argument d'une méthode. Alors, la comparaison telle qu'elle est faite va vérifier les variables \enquote{internes} de \fj{State} alors que nous aimerions laisser l'implémentation libre.
+		
 		La preuve complète des théorèmes a pris plus de temps que prévu, notamment à cause de la structure moins intuitive de la seconde, et elles mériteraient d'être formalisées dans un assistant de preuve comme Coq.
 		
 		La structure de \eng{test interface} peut aussi être utilisée à d'autre fins, par exemple à la définition de librairies, ou de \enquote{modules} dans la terminologie de Java 9+.
@@ -668,9 +721,11 @@
 			// Listes Finies\\
 			\fjclass{List}{}{
 				\fjmethod{Bool}{isEmpty}{}{true}
+				\fjmethod{Object}{ensureFinite}{Object obj}{obj}
 			}\\
 			\fjclass[List]{Cons}{\fjattr[List]{queue}\fjattr{head}}{
 				\fjmethod{Bool}{isEmpty}{}{false}
+				\fjmethod{Object}{ensureFinite}{Object obj}{this.queue.ensureFinite(obj)}
 			}
 		\end{fjlisting}
 	

header.tex

@@ -32,6 +32,8 @@
 \usepackage{enumitem}
 \usepackage{amsfonts}
 
+\usepackage{geometry}
+
 \usepackage{csquotes}
 \usepackage[lighttt]{lmodern}
 \usetikzlibrary{shapes.geometric,positioning}