From 95521344c6da278cd8ec2979935cb41e4f5c7921 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Thu, 18 Aug 2022 04:59:09 +0200 Subject: [PATCH] Typos --- RapportStage.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/RapportStage.tex b/RapportStage.tex index d8ff50f..0aab6cc 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -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}.