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

Typos

Browse Source
This commit is contained in:
Mysaa 2022-08-18 04:59:09 +02:00
parent df93d905ce
commit 95521344c6
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
RapportStage.tex
View File

@ -27,7 +27,7 @@
\subsection{Présentation du problème}
Featherweight Java (abrégé en FJ) \cite{fjdef} est une formalisation de la programmation en orienté objet (POO). Les programmes FJ ont leur syntaxe calquée sur celle du langage Java, et sont compilables avec un compilateur classique. On peut y définir classes, attributs et méthodes, mais pas d'assignation, les objets considérés étant tous immuables.
Le FJ est un bon cas d'étude, variant du λ-calcul, si l'on veut étudier formellement un phénomène d'informatique théorique, comme la compilation, le typage incrémental \cite{kuci_et_al:cocoTypecheck}, la généricité/polymorphisme ou la possession d'objets , et ce dans un langage orienté objet, paradigme utilisé par les langages les plus utilisés de nos jours (Java, Python, C++, ...).
Le FJ est un bon cas d'étude, si l'on veut étudier formellement un phénomène d'informatique théorique, comme la compilation, le typage incrémental \cite{kuci_et_al:cocoTypecheck}, la généricité/polymorphisme ou la possession d'objets , et ce dans un langage orienté objet, paradigme utilisé par les langages les plus utilisés de nos jours (Java, Python, C++, ...).
Nous allons utiliser ce langage pour étudier les équivalences entre des programmes, qui n'ont, à notre connaissance, jamais été étudiées en FJ. Trouver une équivalence, cela signifie essayer de dire formellement que deux programmes \enquote{font la même chose}. Cela peut être utile afin de vérifier si une optimisation temporelle, mémorielle ou sécuritaire d'un programme ne change pas son fonctionnement.
@ -605,7 +605,7 @@
\end{array}
\]
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.
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 \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}.