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

Modifications de l'introduction selon le commentaire de Clément.

Browse Source
This commit is contained in:
Mysaa 2022-08-12 15:28:18 +02:00
parent 98110d6ef8
commit 1cc3b461d9
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
RapportStage.tex
View File

@ -25,10 +25,14 @@
\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.
L'objectif du stage est de définir une équivalence (ou plutôt un préordre) entre les programmes FJ, comme l'on pourrait faire en $\pi$-calcul, et d'essayer d'obtenir des théorèmes utiles sur la nouvelle relation \cite{picalcul_sangiorgi}.
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++, ...).
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.
L'objectif du stage est donc de définir une équivalence (ou plutôt un préordre) entre les programmes FJ, comme l'on pourrait faire en $\pi$-calcul, et d'essayer d'obtenir des théorèmes utiles sur la nouvelle relation \cite{picalcul_sangiorgi}.
\subsection{Motivations de l'étude}
Mes tuteurs de stage, Daniele Varacca et Clément Aubert, ont ensemble écrit un papier qui critiquait la manière peu rigoureuse mais surtout peu réaliste avec laquelle les équivalences entre programmes étaient habituellement définies dans la littérature, et proposent une nouvelle manière qui leur semble \enquote{meilleure} sous plusieurs aspects \cite{papierContextEquiv}.
Mes tuteurs de stage, Daniele Varacca et Clément Aubert, s'interessent aux equivalences de programmes et à comment les \eng{process calculis} peuvent fournir des nouvelles équivalences à d'autres langages \cite{papierContextEquiv}.
Mon objectif était alors de fournir une réflexion sur une étude de cas (le Featherweight Java), afin d'ensuite pouvoir étudier la manière dont mon exploration \enquote{naïve} mais néanmoins approfondie peut-être rapprochée de leur méthode, pouvant ainsi la valider, ou au contraire fournir d'autres éléments afin de la consolider.