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

Prise en compte des commentaires de Daniele

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

29
Bilibibio.bib
View File

@ -68,22 +68,15 @@
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}
@article{papierContextEquiv,
title = {Processes Against Tests: On Defining Contextual Equivalences},
journal = {Journal of Logical and Algebraic Methods in Programming},
pages = {100799},
year = {2022},
issn = {2352-2208},
doi = {https://doi.org/10.1016/j.jlamp.2022.100799},
url = {https://www.sciencedirect.com/science/article/pii/S2352220822000529},
author = {Clément Aubert and Daniele Varacca},
keywords = {Process Algebra, Concurrency, Testing Equivalences, Process Semantics},
abstract = {In this paper, we would like to offer and defend a template to study equivalences between programs—in the particular framework of process algebras for concurrent computation. We believe that our layered model of development will clarify the distinction that is too often left implicit between the tasks and duties of the programmer and of the tester. It will also enlighten pre-existing issues that have been running across process algebras such as the calculus of communicating systems, the π-calculus—also in its distributed version—or mobile ambients. Our distinction starts by subdividing the notion of process in three conceptually separated entities, that we call process terms, (completed) processes and tests, and by stressing the importance of formalizing the completion of process terms and the instrumentation that results from placing a (completed) process into a test. While the role of what can be observed and the subtleties in the definitions of congruences have been intensively studied, the fact that not every term can be tested, and that the tester should have access to a different set of tools than the programmer is curiously left out, or at least not often formally discussed–in this respect, the theory of monitor is a counter-example that we discuss and compare to our approach. We argue that this blind spot comes from the under-specification of contexts—environments in which comparisons occur—that play multiple distinct roles but are generally—at least, on the surface of it—given only one definition that fails to capture all of their aspects.}
}

29
RapportStage.tex
View File

@ -3,10 +3,12 @@
\include{./header.tex}
\title{Vers la définition d'un préordre sur les programmes FeatherweightJava
\title{Définition d'un préordre sur les programmes Featherweight Java
\\[1ex] \large Notes sur mon stage au LACL}
\hypersetup{pdftitle={Vers la définition d'un préordre sur les programmes FeatherweightJava}}
\author{Samy Avrillon, encadré par Daniele Varacca (LACL, UPEC)}
\author{Samy Avrillon, encadré par
\\[1ex] Daniele Varacca (LACL, UPEC)
\\[1ex] et Clément Aubert (Augusta University, Géorgie)}
\begin{document}
@ -23,13 +25,13 @@
Ce document a été réalisé dans le cadre de mon stage réalisé au LACL à Créteil, plus de détails sont donnés en \autoref{anx:stage}.
\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.
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++, ...).
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}.
L'objectif du stage est donc de définir une équivalence (ou plutôt un préordre) entre les programmes FJ 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, s'interessent aux equivalences de programmes et à comment les \eng{process calculis} peuvent fournir des nouvelles équivalences à d'autres langages \cite{papierContextEquiv}.
@ -131,11 +133,12 @@
\subsection{Explication de l'utilité d'un contexte}
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:
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.
Mais le plus gros problème est de déterminer ce qu'est un contexte. La tâche est d'autant plus difficile en Featherweight Java car un programme n'est pas constitué que d'une expression, comme en λ-calcul ou en π-calcul. Une expression seule n'a même aucun sens sans une \eng{class table} associée.
Dans des langages formels basés sur une simple expression, comme le λ-calcul ou le π-calcul, cette notion de contexte fonctionne bien. Il suffit de bien la formaliser puis d'étudier ses propriétés \cite{picalcul_sangiorgi}. Cependant, en FJ, un programme n'est pas constitué que d'une expression. Une expression seule n'a d'ailleurs aucun sens si elle n'est pas associée à une \eng{class table}. Il faut donc construire un contexte qui tienne compte de l'ensemble du programme.
\subsection{Exemples d'équivalences simples}
@ -256,7 +259,7 @@
Nous allons donc créer une structure appelée \eng{test interface} (ou interface de test) qui permet de restreindre les tests à l'utilisation de classes, attributs et méthodes spécifiques. La restriction se fera à l'aide du typage.
Le terme interface n'est pas anodin, la structure ressemble à une interface Java (ou Featherweigth Java \cite{liquori_fjInterfaces}), sauf que les \eng{test interface} ne serviront que lors de la compilation. Une expression va \enquote{compilée} (c'est à dire être typée) avec l'interface, puis sera \enquote{executée} (c'est à dire réduite) avec des vraies \eng{class tables}.
Le terme interface n'est pas anodin, la structure ressemble à une interface Java (que certaines extensions du FJ considèrent \cite{liquori_fjInterfaces}), sauf que les \eng{test interface} ne serviront que lors de la compilation. Une expression va \enquote{compilée} (c'est à dire être typée) avec l'interface, puis sera \enquote{executée} (c'est à dire réduite) avec des vraies \eng{class tables}.
\subsection{Définition de la structure de \eng{test interface}}
@ -543,20 +546,24 @@
Ce théorème se prouve par induction sur la preuve de $\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}$. La preuve est donnée en \autoref{anx:proofTyptyp}.
On peut alors définir un préordre sur les \eng{class tables} de la manière suivante.
On peut alors définir pour chaque \eng{test interface} un préordre sur les \eng{class tables} qui l'implémentent de la manière suivante.
\begin{definition}
Soit une \eng{test interface} $\mathfrak{T}$.
Soit deux \eng{class tables} $\mathcal{A}$ et $\mathcal{B}$ qui implémentent toutes deux $\mathfrak{T}$
\[\mathcal{A} \prec \mathcal{A'} \ssi \forall (\mathcal{B},e) \left|\begin{array}{l}
\[\mathcal{A} \prec_\mathfrak{T} \mathcal{A'} \ssi \forall (\mathcal{B},e) \left|\begin{array}{l}
\mathcal{B} \OKin \mathfrak{T}\\
\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}\\
\mathcal{A}\oplus\mathcal{B} \Downarrow v
\end{array}\right. \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\]
où $\mathcal{A} \oplus \mathcal{B}$ dénote l'ensemble des classes de $\mathcal{A}$ auquel on a ajouté les classes de $\mathcal{B}$ dont les noms n'étaient pas déjà dans $\mathcal{A}$.
\end{definition}
Nous noterons la plupart du temps simplement $\prec$ pour désigner $\prec_\mathfrak{T}$ si la \eng{test interface} considérée est sans ambiguïté.
Nous allons d'abord renforcer un peu ce préordre, avant de fournir un exemple complet \autoref{sec:exPreordre}.
\subsection{Renforcement de ce préordre avec les valeurs infinies}
@ -613,7 +620,7 @@
Intuitivement, on vérifie que si d'un coté du préordre, l'expression peut s'évaluer en un objet de type \fj{C}, alors l'autre coté s'évaluera lui aussi en un objet de type \fj{C}, et ce récursivement.
On change ainsi la définition de tous les autres préordres, notamment celui sur les \eng{class tables}:
On change ainsi dans la définition précédente du préordre sur les \eng{class tables}, mais aussi dans tout autre préordre \enquote{simple} que l'on aurait pu définir:
\[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\]
Nous allons maintenant étudier les propriétés de cette nouvelle définition du préordre.