From 98110d6ef87322b4f4afa5e5f9a9b9aed61781aa Mon Sep 17 00:00:00 2001 From: Mysaa Date: Fri, 12 Aug 2022 14:16:57 +0200 Subject: [PATCH] Correction de quelques erreurs LaTeX --- Bilibibio.bib | 19 +++++++++++++++++++ RapportStage.tex | 14 +++++++------- 2 files changed, 26 insertions(+), 7 deletions(-) diff --git a/Bilibibio.bib b/Bilibibio.bib index bd83e5b..6cf11cf 100644 --- a/Bilibibio.bib +++ b/Bilibibio.bib @@ -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} } \ No newline at end of file diff --git a/RapportStage.tex b/RapportStage.tex index 9ab3f64..0242eb0 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -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})}}