Ajout d'une citation.

This commit is contained in:
Mysaa 2022-08-14 02:00:30 +02:00
parent 396db085ec
commit ee742cb8a6
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F

View File

@ -25,7 +25,7 @@
\subsection{Présentation du problème}
Featherweight Java (abrégé en FJ) \cite{fjdef} est une formalisation, à l'instar du $\lambda$-calcul ou du $\pi$-calcul de la programmation en orienté objet (POO). Les programmes FJ ont leur syntaxe calquée depuis le language Java, et sont compilables avec un compilateur. 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, 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, 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++, ...).
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.