Correction de quelques erreurs LaTeX
This commit is contained in:
parent
ca485e2e77
commit
98110d6ef8
GPG Key ID:
7054D5D6A90F084F
@ -67,4 +67,23 @@
|
||||
URN = {urn:nbn:de:0030-drops-72628},
|
||||
doi = {10.4230/LIPIcs.ECOOP.2017.18},
|
||||
annote = {Keywords: type checking, co-contextual, constraints, class table, Featherweight Java}
|
||||
}
|
||||
@inproceedings{papierContextEquiv,
|
||||
author = {Cl{\'{e}}ment Aubert and
|
||||
Daniele Varacca},
|
||||
editor = {Julien Lange and
|
||||
Anastasia Mavridou and
|
||||
Larisa Safina and
|
||||
Alceste Scalas},
|
||||
title = {Process, Systems and Tests: Three Layers in Concurrent Computation},
|
||||
booktitle = {Proceedings 14th Interaction and Concurrency Experience, {ICE} 2021,
|
||||
Online, 18th June 2021},
|
||||
series = {{EPTCS}},
|
||||
volume = {347},
|
||||
pages = {1--21},
|
||||
year = {2021},
|
||||
doi = {10.4204/EPTCS.347.1},
|
||||
timestamp = {Mon, 29 Nov 2021 16:32:06 +0100},
|
||||
biburl = {https://dblp.org/rec/journals/corr/abs-2007-08187.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
@ -115,7 +115,7 @@
|
||||
|
||||
Enfin nous définissons plusieurs classes qui permettent de coder de façon plus abstraite, dont les définitions complètes sont données en \autoref{anx:moreclass}.
|
||||
|
||||
La première classe définie est la classe \fj{Bool}, liée à deux objets notés \fj{true} et \fj{false}. Cette classe met à disposition une méthode \enquote{if then else} \fj{ite(Object,Object)} telle que \fj{true.ite($e_t$,$e_f$)} renvoie $e_t$ et \fj{false.ite($e_t$,$e_f$)} renvoie $e_f$.
|
||||
La première classe définie est la classe \fj{Bool}, liée à deux objets notés \fj{true} et \fj{false}. Cette classe met à disposition une méthode \enquote{if then else} \fj{ite(Object,Object)} construite telle que \fj{true.ite($e_t$,$e_f$)} renvoie $e_t$ et \fj{false.ite($e_t$,$e_f$)} renvoie $e_f$.
|
||||
|
||||
La seconde classe est \fj{Int}, liée à des objets notés \fj{0}, \fj{1}, \fj{2}, \dots. Cette classe met a disposition une méthode \fj{Bool isZero()} qui renvoie \fj{true} si l'objet appelant est zéro, et renvoie \fj{false} sinon. Plusieurs méthodes sont définies en sus dans la définition complète présentée en \autoref{anx:moreclass} permettant de manipuler ces objets.%TODO Vérifier qu'elles le soient
|
||||
|
||||
@ -139,7 +139,7 @@
|
||||
|
||||
\subsection{Explication de l'utilité d'un contexte}
|
||||
|
||||
Les équivalences entre les programmes sont habituellement définies en utilisant des \enquote{contextes}. Deux programmes sont dits équivalents lorsqu'ils donnent les mêmes résultats sous tout contexte. Pour un contexte $C$, on va noter $C\bracket{P}$ l'interprétation d'un programme $P$ dans le contexte. Alors, le préordre sera défini comme tel:
|
||||
Les équivalences entre les programmes sont habituellement définies en utilisant des structures appelées \enquote{contextes}. Deux programmes sont dits équivalents lorsqu'ils donnent les mêmes résultats sous tout contexte. Pour un contexte $C$, on va noter $C\bracket{P}$ l'interprétation d'un programme $P$ dans le contexte. Alors, le préordre sera défini comme tel:
|
||||
\[P\prec Q \ssi \forall C\quad C\bracket{P}\Downarrow v \implies C\bracket{Q}\Downarrow v\]
|
||||
On confondra souvent les termes \enquote{équivalence} et \enquote{préordre} dans la suite de ce document, car le premier est plus pratique pour visualiser l'utilité des constructions établies.
|
||||
|
||||
@ -269,17 +269,17 @@
|
||||
|
||||
\begin{figure}
|
||||
\begin{fjlisting}
|
||||
Number \{\}\\
|
||||
Number \{\}\\\null
|
||||
|
||||
Int \{\}\\
|
||||
Int : Int suivant(Int)\\
|
||||
Int : Int add(Int,Int)\\
|
||||
Int <: Number\\
|
||||
Int <: Number\\\null
|
||||
|
||||
Frac(Int numerateur, Int denominateur)\\
|
||||
Frac : Frac inverted()\\
|
||||
Frac : Int floor()\\
|
||||
Frac <: Number\\
|
||||
Frac <: Number\\\null
|
||||
|
||||
RichInt \{Int value\}\\
|
||||
RichInt : Int getInt()\\
|
||||
@ -292,7 +292,7 @@
|
||||
À cette grammaire, nous allons ajouter quelques règles afin que la \eng{test interface} soit considérée comme valide. Dans la suite du document, on considèrera que toutes les \eng{test interfaces} utilisées sont toujours valides. Ces règles sont les suivantes:
|
||||
|
||||
\begin{itemize}
|
||||
\item Chaque nom de classe est défini au plus une fois par une \autoref{rule:tsg:attributes} ou une \autoref{rule:tsg:constructor}.
|
||||
\item Chaque nom de classe est défini au plus une fois par ou bien une \autoref{rule:tsg:attributes} ou bien une \autoref{rule:tsg:constructor}.
|
||||
\item Chaque nom de methode est défini au plus une fois par nom de classe par une \autoref{rule:tsg:method}.
|
||||
\item Les noms de classe utilisés sont définis (sauf éventuellement \fj{Object}).
|
||||
\end{itemize}
|
||||
@ -809,7 +809,7 @@
|
||||
|
||||
\paragraph{Troisième propritété}
|
||||
|
||||
Une dernière fois, inversons la règle qui a permis de prouver $\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}}$.
|
||||
Une dernière fois, inversons la règle qui a permis de prouver : \[\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}}\]
|
||||
|
||||
\subparagraph{Cas $\left[\fj{Cc ($\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-construct})}}
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user