Mysaa/stage-2022
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Ever more typos

Browse Source
This commit is contained in:
Mysaa 2022-08-07 15:34:42 +02:00
parent 380b23f527
commit e4178b644b
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
RapportStage.tex
View File

@ -261,7 +261,7 @@
Int \{\}\\
Int : Int suivant(Int)\\
Int : Int add(Int,Int)\\
Int <: Number\\++
Int <: Number\\
Frac(Int numerateur, Int denominateur)\\
Frac : Frac inverted()\\
@ -291,7 +291,6 @@
Il peut sembler au premier abord qu'il manque à cette définition des \eng{test interfaces} une façon d'autoriser le programmeur à utiliser un constructeur, sans en imposer l'ordre des paramètres, mais en autorisant l'accès à certains attributs. Pourtant, si l'on peut construire et accéder à un certain attribut \fj{field} sur un type \fj{C}, et que l'objet est constructible, c'est à dire qu'il existe une expression \fj{new C(new P1($e_1$),...,new Pn($e_n$))}, alors on peut créer une expression qui nous indique la position dans le constructeur de l'attribut.
Pour ce faire, il faut, pour chaque nom de classe \fj{Pk} des paramètres, créer une sous-classe \fj{Pk\_k} (les \fj{Pk} pouvaient se confondre, mais les \fj{Pk\_k} sont tous distincts). Alors la construction suivante renverra une valeur de type \fj{Pj\_k}, et on aura ainsi accès à la position dans le constructeur de l'attribut \fj{field}.
\[\fj{new C(new P1_1($e_1$),new P2_2($e_2$),...,new Pn_n($e_n$)).field}\]
% TODO Ajouter une note sur l'abscence de tolérance lorsque les champs sont spécifiés.
Nous allons aussi considérer uniquement les \eng{test interface} pour lesquelles il existe au moins une \eng{class table} les implémentant. Cela impose certaines règles, notamment que l'opération $\subclass$ induite puisse créer un bon ordre, mais d'autres contraintes plus complexes à exprimer apparaîssent, nous n'allons pas chercher à les exprimer ici, mais vous trouverez des exemples de telles \eng{test interfaces} en \autoref{fig:tiUnsolvable}
@ -324,6 +323,7 @@
\end{fjlisting}
\end{tabular}
\end{center}
%TODO Ajouter une courte explication de pourquoi
\caption{Exemples de \textit{test interfaces} implémentés par aucune \textit{class table}}
\label{fig:tiUnsolvable}
\end{figure}
@ -559,7 +559,6 @@
&\rightarrow& \fj{0}
\end{array}
\]
% TODO faut-il adapter l'exemple aux test interfaces au risque de trop surcharger ?
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\]
@ -583,7 +582,7 @@
Nous allons maintenant étudier les propriétés de cette nouvelle définition du préordre.
\begin{property}
\[\forall \hbar \forall \overline{e} \quad \hbar\left[\overline{e}\right]\rightarrow e' \implies \exists \overline{e''}\quad e' = \hbar\left[\overline{e''}\right]\]
\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
\end{property}
On peut prouver cette propriété inductivement en montrant qu'une expression ayant un nœud \enquote{\fj{new}} en nœud racine se réduira forcément en une expression ayant un nœud racine du même type, en inversant la relation de réduction.