Ajout d'un exemple de la puissance de la compairaison des class table vis-à-vis des programmes.
This commit is contained in:
parent
24544df6ff
commit
c6e5368993
@ -224,7 +224,31 @@
|
||||
Tous les tests présentés dans la section précédente visaient à tester un programme entier (une \eng{class table} et une expression). Il semble cependant étrange de procéder ainsi. En effet, un développeur souhaitera principalement comparer entre elles des librairies, ce qui correspondrait à nos \eng{class tables}. On ne cherche plus à savoir si deux programmes \enquote{font la même chose}, mais plutôt est-ce que ces deux \eng{class tables} fournissent les mêmes fonctions.
|
||||
|
||||
En bonus, l'étude des \eng{class tables} est tout aussi complète que l'étude des programmes entiers, car nous pouvons toujours rajouter une classe \fj{Main} qui n'aie qu'une méthode \fj{Main.main} dont le corps soit l'expression de notre programme. Alors tester cette nouvelle \eng{class table} reviendra à tester le programme entier.
|
||||
%TODO Ajouter un exemple, ou faire un théorème
|
||||
|
||||
\begin{center}
|
||||
\begin{multicols}{2}
|
||||
\null\vfill
|
||||
\begin{fjlisting}[width=.4\textwidth]
|
||||
class XXX extends XXX \{\\
|
||||
\}\\
|
||||
\vdots\\
|
||||
\fjmain{expression}
|
||||
\end{fjlisting}
|
||||
\vfill\null
|
||||
\columnbreak
|
||||
\null\vfill
|
||||
\begin{fjlisting}[width=.4\textwidth]
|
||||
class XXX extends XXX \{\\
|
||||
\}\\
|
||||
\vdots\\
|
||||
\fjclass{Main}{}{
|
||||
\fjmethod{Object}{main}{}{expression}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\vfill\null
|
||||
\end{multicols}
|
||||
\end{center}
|
||||
Alors, on a transformé le \emph{programme} en \emph{\eng{class table}}, et si nou voulons tester le main du programme, il suffit de tester ce que renvoie l'expression \fj{new Main().main()}, qui se réduit en une étape en le main du programme.
|
||||
|
||||
\paragraph{Idée d'une nouvelle structure}
|
||||
|
||||
@ -575,8 +599,8 @@
|
||||
Nous avons l'impression que certaines expressions forment des sortes de \enquote{valeurs infinies}, qui peuvent quand même être utilisées dans des programmes, mais uniquement de manière finie. Nous allons donc changer la définition de tous nos préordres, en remplaçant les propositions de la forme suivante.
|
||||
\[\forall v\quad (\mathcal{A}, e) \Downarrow v \implies (\mathcal{B}, f) \Downarrow v\]
|
||||
|
||||
Nous allons tout d'abord définir une nouvelle grammaire, celle des \enquote{valeurs ouvertes} ou \enquote{valeurs avec variables}, que l'on notera avec la lettre $\hbar$. Il s'agit simplement d'expressions ouvertes qui ne contiennent que des nœuds de type \textsc{E-Var} et \textsc{E-Cstr} et telles que un nom de variable n'est utilisé au plus qu'\emph{une seule fois}.
|
||||
%TODO Rajouter des références sur ces deux noms de règles
|
||||
Nous allons tout d'abord définir une nouvelle grammaire, celle des \enquote{valeurs ouvertes} ou \enquote{valeurs avec variables}, que l'on notera avec la lettre $\hbar$. Il s'agit simplement d'expressions ouvertes qui ne contiennent que des nœuds de type \ref{rule:expr:variable} et \ref{rule:expr:constructor} et telles que un nom de variable n'est utilisé au plus qu'\emph{une seule fois}.
|
||||
|
||||
Par exemple, l'objet suivant est une valeur à trois variables
|
||||
\[\fj{new C(x,new S(new S(y,new G()),z))}\]
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user