Premier commit - Notes
This commit is contained in:
commit
4c5fd08211
GPG Key ID:
7054D5D6A90F084F
53
NotesStage.bib
Normal file
53
NotesStage.bib
Normal file
@ -0,0 +1,53 @@
|
||||
@article{fjdef,
|
||||
author = {Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip},
|
||||
title = {Featherweight Java: A Minimal Core Calculus for Java and GJ},
|
||||
year = {2001},
|
||||
issue_date = {May 2001},
|
||||
publisher = {Association for Computing Machinery},
|
||||
address = {New York, NY, USA},
|
||||
volume = {23},
|
||||
number = {3},
|
||||
issn = {0164-0925},
|
||||
url = {https://doi.org/10.1145/503502.503505},
|
||||
doi = {10.1145/503502.503505},
|
||||
abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.},
|
||||
journal = {ACM Trans. Program. Lang. Syst.},
|
||||
month = {may},
|
||||
pages = {396–450},
|
||||
numpages = {55},
|
||||
keywords = {generic classes, language design, language semantics, Java, Compilation}
|
||||
}
|
||||
@website{yingfei_2014,
|
||||
title={Chapter 19: Case study: Featherweight java - github pages}, url={https://xiongyingfei.github.io/DPPL/2014/zhao_ch19.pdf},
|
||||
journal={A quick tour of OCaml},
|
||||
publisher={Peking University},
|
||||
author={Yingfei, Xiong},
|
||||
year={2014}
|
||||
}
|
||||
@book{picalcul_sangiorgi,
|
||||
author = {Sangiorgi, Davide and Walker, David},
|
||||
title = {PI-Calculus: A Theory of Mobile Processes},
|
||||
year = {2001},
|
||||
isbn = {0521781779},
|
||||
publisher = {Cambridge University Press},
|
||||
address = {USA},
|
||||
abstract = {From the Publisher:Mobile systems, whose components communicate and change their structure, now pervade the informational world and the wider world of which it is a part. The science of mobile systems is as yet immature, however. This book presents the pi-calculus, a theory of mobile systems. The pi-calculus provides a conceptual framework for understanding mobility, and mathematical tools for expressing systems and reasoning about their behaviors. The book serves both as a reference for the theory and as an extended demonstration of how to use pi-calculus to describe systems and analyze their properties. It covers the basic theory of pi-calculus, typed pi-calculi, higher-order processes, the relationship between pi-calculus and lambda-calculus, and applications of pi-calculus to object-oriented design and programming. The book is written at the graduate level, assuming no prior acquaintance with the subject, and is intended for computer scientists interested in mobile systems.}
|
||||
}
|
||||
@article{liquori_fjInterfaces,
|
||||
TITLE = {{Extending FeatherTrait Java with Interfaces}},
|
||||
AUTHOR = {Liquori, Luigi and Spiwack, Arnaud},
|
||||
URL = {https://hal.inria.fr/inria-00432540},
|
||||
JOURNAL = {{Theoretical Computer Science}},
|
||||
PUBLISHER = {{Elsevier}},
|
||||
SERIES = {Theoretical Computer Science},
|
||||
VOLUME = {30},
|
||||
NUMBER = {1-3},
|
||||
PAGES = {243--260},
|
||||
YEAR = {2008},
|
||||
MONTH = May,
|
||||
DOI = {10.1016/j.tcs.2008.01.051},
|
||||
KEYWORDS = {Object-oriented language design ; inheritance ; types},
|
||||
PDF = {https://hal.inria.fr/inria-00432540/file/TCS-60.pdf},
|
||||
HAL_ID = {inria-00432540},
|
||||
HAL_VERSION = {v1},
|
||||
}
|
||||
559
NotesStage.tex
Normal file
559
NotesStage.tex
Normal file
@ -0,0 +1,559 @@
|
||||
\documentclass[10pt,a4paper,draft]{article}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amssymb}
|
||||
\usepackage{bbm}
|
||||
\usepackage{stmaryrd}
|
||||
\usepackage[french]{babel}
|
||||
\usepackage{csquotes}
|
||||
\usepackage{listings}
|
||||
\usepackage{lstautogobble}
|
||||
\usepackage{algorithm2e}
|
||||
\usepackage{svg}
|
||||
\usepackage{tikz}
|
||||
\usepackage{tcolorbox}
|
||||
\usepackage{mdframed}
|
||||
\usepackage{proof}
|
||||
\usepackage[lighttt]{lmodern}
|
||||
|
||||
\newcommand{\pgrph}{\P}
|
||||
\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}}
|
||||
\renewcommand{\P}{\mathbb{P}}
|
||||
\newcommand{\E}{\mathbb{E}}
|
||||
\newcommand{\1}{\scalebox{1.2}{$\mathbbm{1}$}}
|
||||
\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor}
|
||||
\newcommand{\littleO}{o}
|
||||
\newcommand{\bigO}{\mathcal{O}}
|
||||
\newcommand{\longdash}{\:\textrm{---}\:}
|
||||
|
||||
\DeclareMathOperator{\new}{\text{\textbf{new}}}
|
||||
\DeclareMathOperator{\CT}{CT}
|
||||
\let\rbar\bar
|
||||
\let\bar\overline
|
||||
\newcommand\subclass{<:}
|
||||
|
||||
\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
|
||||
|
||||
\newtheorem{theorem}{Theorem}
|
||||
|
||||
\tcbuselibrary{fitting}
|
||||
|
||||
\newtcbox{\fjmaincodebox}{nobeforeafter,tcbox raise base, arc=0pt, outer arc=0pt, boxsep=0pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=0pt,colback=white!85!black}
|
||||
\newtcolorbox{fjcodebox}{left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!96!black}
|
||||
|
||||
\newenvironment{fjlisting}
|
||||
{
|
||||
%\begin{center}
|
||||
\fjcodebox
|
||||
\ttfamily
|
||||
}{
|
||||
\endfjcodebox
|
||||
%\end{center}
|
||||
}
|
||||
\newcommand{\ifnullthenelse}[3]{
|
||||
\ifnum\value{#1}=0
|
||||
#2
|
||||
\else
|
||||
#3
|
||||
\fi
|
||||
}
|
||||
|
||||
\makeatletter
|
||||
\newcommand*\idstyle{%
|
||||
\expandafter\id@style\the\lst@token\relax
|
||||
}
|
||||
\def\id@style#1#2\relax{%
|
||||
\ifcat#1\relax\else
|
||||
\ifnum`#1=\lccode`#1%
|
||||
\ttfamily\slshape
|
||||
\fi
|
||||
\fi
|
||||
}
|
||||
\makeatother
|
||||
|
||||
\lstdefinelanguage{FeatherweightJava}{
|
||||
keywords = {new, this},
|
||||
basicstyle=\ttfamily,
|
||||
identifierstyle=\idstyle,
|
||||
mathescape=true
|
||||
}
|
||||
\newcommand{\fj}[1]{\text{\lstinline[language=FeatherweightJava,mathescape=true]|#1|}}
|
||||
|
||||
\newcounter{fjargcount}
|
||||
\newcommand{\fjparamattributes}[2][Object]{
|
||||
\null\qquad #1 #2;\newline
|
||||
}
|
||||
\newcommand{\printcomma}{,}
|
||||
\newcommand{\fjparamconstparameters}[2][Object]{
|
||||
\ifnullthenelse{fjargcount}{}{,} \text{#1} \;\text{#2}
|
||||
\stepcounter{fjargcount}
|
||||
}
|
||||
\newcommand{\fjparamconstassign}[2][Object]{
|
||||
\null\qquad\qquad \textbf{this}.#2 = #2;\newline
|
||||
}
|
||||
\newcommand{\method}[4]{
|
||||
\null\qquad #1 #2(#3)\{\newline
|
||||
\null\qquad\qquad \textbf{return} \lstinline[language=Java]{#4};\newline
|
||||
\null\qquad\}\newline
|
||||
}
|
||||
|
||||
\newcommand{\fjmain}[1]{
|
||||
\noindent\fjmaincodebox{\lstinline[language=Java]{#1}}
|
||||
}
|
||||
|
||||
% Premier argument: Nom de la classe
|
||||
% Second argument: \attr{x}[Object] \attr{attr}[A]
|
||||
% Troisième argument \method{C}{metname}{Object w, B par}{((D)obj).apply(par)} plusieurs fois
|
||||
% Argument optionnel: la classe que l'on extend
|
||||
\newcommand{\fjclass}[4][Object]{%
|
||||
\noindent \textbf{class} #2 \textbf{extends} #1 \{\newline
|
||||
% Attributs
|
||||
\let\attr\fjparamattributes
|
||||
#3
|
||||
% Constructeur
|
||||
\let\attr\fjparamconstparameters
|
||||
\setcounter{fjargcount}{0}
|
||||
\null\qquad #2(\ifx&\else $#3$\fi) \{\newline
|
||||
\null\qquad\qquad \textbf{super}();\newline
|
||||
\let\attr\fjparamconstassign%
|
||||
#3
|
||||
\null\qquad\}\\
|
||||
% Méthodes
|
||||
#4
|
||||
\}\newline
|
||||
}
|
||||
|
||||
\title{Notes de Stage}
|
||||
\author{Samy Avrillon}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\maketitle
|
||||
|
||||
\hsep
|
||||
|
||||
\tableofcontents
|
||||
|
||||
\newpage
|
||||
|
||||
\section{Tentatives de définition d'un contexte sur Featherweight Java}
|
||||
|
||||
\subsection{Définitions et notations}
|
||||
|
||||
On se base sur les notations issues de la définition du Featherweight Java \cite{fjdef}.
|
||||
Donc $e$ est la grammaire des expressions, $L$ la grammaire des classes, $\bar{x}$ dénote une suite potentiellement vide d'élément de type $x$, \verb*|<:| désigne la relation de sous-typage, $\longrightarrow$ désigne l'opérateur de réduction.
|
||||
|
||||
Un programme Featherweight Java est composé de deux parties: La première est une liste de définitons de classes, que le papier originel appelait \textit{collection of class definitions}, mais que nous appellerons plutôt \textit{Class Tables} \cite{yingfei_2014}. La seconde est une expression à évaluer (on peut la voir comme le body d'une fonction \fj{main} d'un programmme Java). Nous allons donc considérer qu'un programme FeatherweightJava $P$ est un couple $(\bar{L},e)$, et l'on notera $\CT(P) = \bar{L}$ et $e_P = e$ lorsque nous manipulerons plusieurs programmes.
|
||||
|
||||
On note la gramaire à un trou $h$ :
|
||||
$$h := x | [.] | h.f | h.m(\bar{e}) | e.m(\bar{e},h,\bar{e}) | \new C(\bar{e},h,\bar{e}) | (C) h $$
|
||||
|
||||
On pourra souvent se ramener à la grammaire à plusieurs trous $\tilde{h}$ :
|
||||
$$\tilde{h} := x | [.] | \tilde{h}.f | \tilde{h}.m(\bar{\tilde{h}}) | \new C(\bar{\tilde{h}}) | (C) h | e $$
|
||||
|
||||
Puis on ajoute l'opération de \textit{remplissage} $h[g]$ pour $h$ expression à trou et $g$ expression classique, définie récursivement:
|
||||
|
||||
\begin{align*}
|
||||
x[g] &= x\\
|
||||
[.][g] &= g\\
|
||||
(h.f)[g] &= h[g].f\\
|
||||
(h.m(\bar{e}))[g] &= h[g].m(\bar{e})\\
|
||||
(e.m(\bar{e},h,\bar{e}))[g] &= e.m(\bar{e},h[g],\bar{e})\\
|
||||
(\new C(\bar{e},h,\bar{e}))[g] &= \new C(\bar{e},h[g],\bar{e})\\
|
||||
((C) h)[g] &= (C) h[g]
|
||||
\end{align*}
|
||||
|
||||
\subsection{Première définition naïve}
|
||||
|
||||
La première définition, à l'instar de celle donnée pour le $\pi$-calcul pourrait ressembler à ça:
|
||||
|
||||
Un contexte est un élément de $h$.
|
||||
|
||||
Alors l'interprétation d'un programme dans un contexte est $C[P] = (CL(P), h[e])$
|
||||
|
||||
Le problème, c'est que cette version des contextes est peu puissante. En effet, puisque nous avons juste des expressions, nous limitons à l'utilisation de la class table du programme. Et ça nous enlève tout une batterie de tests que l'on aurait pu autrement pû utiliser.
|
||||
|
||||
\subsubsection{Problème du trou dégénéré}
|
||||
|
||||
\begin{theorem}
|
||||
Si la class table du programme testé permet de créer un trou dégénéré, c'est à dire un contexte à trou te que pour toute expression $e$, il existe une expression trouée $h$ telle que $\forall p \; h[p] \rightarrow^* e$.
|
||||
|
||||
Alors $P\leqslant Q \implies \CT(P) \subseteq \CT(Q)$
|
||||
\end{theorem}
|
||||
|
||||
Un exemple classique de contexte ayant un trou dégénéré est dans un programme dont la class table contient la classe \fj{Pair} suivante:
|
||||
\begin{fjlisting}
|
||||
\fjclass{Pair}{
|
||||
\attr{fst}
|
||||
\attr{snd}
|
||||
}{}
|
||||
\end{fjlisting}
|
||||
|
||||
Alors si on considère le contexte $C$ = \fj{new Pair(e,[.]).fst} pour toute expression \fj{e}. on aura $C[p]$ = \fj{new Pair(e,p).fst} $\rightarrow^*$ \fj{e}.
|
||||
|
||||
Le théorème se prouve en construisant des expressions qui dépendent explicitement de la structure des classes: \fj{new A()} ne se résout en une valeur seulement si la class table contient une classe A sans attributs, \fj{new C(new A(), new B()).m(new A())} impose les attributs de C ainsi que l'existence d'une méthode m prenant un argument A, et cætera.
|
||||
|
||||
\paragraph{C'est un problème} par ce que deux programmes ne peuvent pas utiliser des classes internes différentes. Par exemple, un programme de tri d'un liste qui utiliserait une classe \fj{Map} et un autre qui utiliserait \fj{Tree} ne pourraient être comparés, quand bien même leurs fonctionnement pourrait paraître similaire à nos yeux. On a le même problème sur le nom des classes «internes».
|
||||
|
||||
\paragraph{Ce n'est pas un problème} car sans notion d'access control, un utilisateur peut utiliser toutes les classes internes. Donc la structure interne du programme a de l'importance sur ce qu'on peut modifier du programme.
|
||||
|
||||
\paragraph{Une solution} serait de redéfinir le préordre pour ne considérer que les classes sur les parties des class tables qui sont en commun. Par contre, on ne résout pas le problème de la dépendance au nom, si deux programmes définissent une meme classe \fj{MaClasse}, doit-on imposer pour les programmes soient équivalents que les deux «implémentations» le soient ?
|
||||
|
||||
\paragraph{Une autre solution} pourrait être de comparer uniquement avec des contextes qui «utiliseraient» (notion à définir) une partie spécifique de la Class Table qui serait alors comparée. On retrouve l'idée d'interface présente dans le Java complet (ou d'autres versions de FJ \cite{liquori_fjInterfaces}).
|
||||
|
||||
\paragraph{Une dernière solution} serait d'ailleurs d'ajouter les access control au featherweight java, c'est à dire de pouvoir noter les classes comme \fj{public}, \fj{private}, \fj{package-protected} ou \fj{protected}, en restreignant directement le typage des sexpressions.
|
||||
|
||||
|
||||
\subsection{Seconde définiton naïve}
|
||||
|
||||
Un contexte est une class table $\bar{L}$ et un contexte à trou $h$.
|
||||
|
||||
Alors $C[P] = (\CT(P) + \bar{L}', h[\bar{L}'/\bar{L}][e_P])$ où $\bar{L}'$ est une class table $\alpha$-convertible en $\bar{L}$ tel qu'aucun nom de classe ne coïncide avec ceux de $\CT(P)$.
|
||||
|
||||
On définit un $\alpha$-renommage de classe dans une class table comme l'opération de changer un nom de classe en un autre nom, en changant toutes les occurences de ce nom ($\new C(\dots)$, $(C) e$, \textbf{extends}, définition d'attributs, de paramètres de méthodes et de type de retour de méthode), en s'assurant que le nom n'était pas utilisé.
|
||||
|
||||
Deux class tables sont alors $\alpha$-convertibles si on peut passer de l'une à l'autre avec un nombre fini d'$\alpha$-renommages, à l'instar de ce qui est fait dans le $\pi$-calcul \cite{picalcul_sangiorgi}.
|
||||
|
||||
On a alors forcément un trou dégénéré (parce que on peut ajouter la classe Paire nous-même)
|
||||
|
||||
\subsection{Troisième définition naïve}
|
||||
Un contexte est une class table $\bar{L}$ et une expression $e_C$.
|
||||
|
||||
Alors $C[P] = (\CT(P) + \bar{L}' + Main'', e_C[CT'/CT][Main''/Main])$ où $\bar{L}'$ est obtenu de la même manière que précédement et $Main$ est la class table suivante:
|
||||
|
||||
\begin{fjlisting}
|
||||
\fjclass{Main}{}{
|
||||
\method{Object}{main}{Object $\bar{x}$}{e}
|
||||
}
|
||||
\end{fjlisting}
|
||||
|
||||
où $\bar{x}$ est l'ensemble des variable libres de $e_P$.
|
||||
|
||||
On sent que l'on veut tester l'utilisation d'une méthode plutôt que d'une expression, ce qui est en adéquation avec le paradigme orienté objet, mais ces contextes restent toujours aussi faillibles.
|
||||
|
||||
On peut forcer un peu plus l'utilisation du main, en construisant le contexte dans sa version 3.1:
|
||||
$C$ = $\bar{L}$ et $\bar{e_C}$ interprété en
|
||||
$$C[P] = (\CT(P) + \bar{L}' + Main'', \new Main().main(\bar{e_C[CT'/CT][Main''/Main])})$$
|
||||
|
||||
\subsection{Quatrième définition naïve}
|
||||
La première méthode naïve est utile pour faire des équivalences entre des programmes de même class table. Mais on pourrait faire mieux.
|
||||
|
||||
On définit déjà un préordre sur les class tables:
|
||||
|
||||
$$ CTA \prec CTB \iff \forall e \forall v (CTA,e)\Downarrow v \implies (CTB,e)\Downarrow v$$
|
||||
|
||||
On peut ainsi utiliser la méthode du contexte pour créer un pré-ordre sur les programmes:
|
||||
|
||||
$$ P \prec Q \iff \CT(P) \prec \CT(Q) \text{ et } \forall h (\CT(P),h[e_P])\Downarrow v \implies (\CT(Q), h[e_Q])\Downarrow v$$
|
||||
|
||||
On peut aussi encore augmenter le contexte en le définissant avec sa propre class table:
|
||||
|
||||
Un contexte $C$ est alors une CT $\bar{L}$ et une expression trouée $h$.
|
||||
|
||||
L'interpretation est alors $C[P] = (CT(C),h[e_P])$ si $\CT(P) \prec \CT(C)$. On dit alors que $C$ convient à $P$.
|
||||
|
||||
On a alors un nouveau pré-ordre sur les programmes:
|
||||
|
||||
$$P\prec Q \iff \forall C (C \text{ convient à } P\text{ et }C \text{ convient à } Q) \implies \left(\forall v\; C[P]\Downarrow v \implies C[Q]\Downarrow v\right)$$
|
||||
|
||||
\paragraph{Gros problème cependant} si les deux programmes comparées n'ont aucun contexte qui leur convienne à tous les deux. On est alors bloqués dans une situation d'universalité du vide. Par exemple les deux class table suivantes, notées $CT_A$ et $CT_B$:
|
||||
|
||||
\noindent
|
||||
\begin{minipage}{.5\textwidth}
|
||||
\begin{fjlisting}
|
||||
\fjclass{A}{}{}
|
||||
\fjclass{B}{}{}
|
||||
\fjclass{Get}{
|
||||
\attr[A]{a}
|
||||
\attr[B]{b}
|
||||
}{
|
||||
\method{Object}{get}{}{this.a}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\end{minipage}
|
||||
\begin{minipage}{.5\textwidth}
|
||||
\begin{fjlisting}
|
||||
\fjclass{A}{}{}
|
||||
\fjclass{B}{}{}
|
||||
\fjclass{Get}{
|
||||
\attr[A]{a}
|
||||
\attr[B]{b}
|
||||
}{
|
||||
\method{Object}{get}{}{this.b}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\end{minipage}
|
||||
\\
|
||||
Alors en notant $e_A = \fj{(A)(new Get(new A(), new B()).get())}$ et $e_B = \fj{(B)(new Get(new A(), new B()).get())}$, on a
|
||||
|
||||
$$(CL_A,e_A)\Downarrow \new A(); (CL_A,e_B)\not\Downarrow ; (CL_B,e_A)\not\Downarrow ; (CL_B,e_B)\Downarrow \new B()$$
|
||||
|
||||
Donc aucun contexte ne peut satisfaire les deux class tables. Ce qui est problématique !
|
||||
|
||||
On peut déjà chercher à simplifier le programme, afin d'enlever les opérations inutiles quand elles ne sont pas au cœur des opérations. Par exemple, dans le cas d'un programme totalement légitime, l'ajout de ces deux classes annulerai tout le travail, même si elles ne sont pas utilisées.
|
||||
|
||||
On définit qu'un programme $P'$ est plus simple que $P$, noté $P' < P$ par trois axiomes:
|
||||
\begin{enumerate}
|
||||
\item $\CT(P') \prec \CT(P)$
|
||||
\item $e_{P'} = e_{P}$
|
||||
\item $\forall v\; P\Downarrow v \implies P'\Downarrow v$
|
||||
\end{enumerate}
|
||||
|
||||
|
||||
|
||||
\section{Définir l'équivalence sur les expressions}
|
||||
|
||||
|
||||
Nous avions déjà défini le préordre suivant sur les Class Tables:
|
||||
$$ CTA \prec CTB \iff \forall e \forall v (CTA,e)\Downarrow v \implies (CTB,e)\Downarrow v$$
|
||||
|
||||
Mais cette définition pose deux problèmes:
|
||||
\begin{itemize}
|
||||
\item On n'a toujours pas de préordre sur les programmes entiers, ni sur les expressions.
|
||||
\item Cette définition sémantique est difficile à vérifier, il nous faudrait une caractérisation de cette équivalence plus simple à vérifier en pratique.
|
||||
\end{itemize}
|
||||
|
||||
\subsection{Une équivalence naïve}
|
||||
|
||||
Si l'on souhaitait comparer deux expressions de but en blanc, dans une class table donnée.
|
||||
|
||||
La version de l'expression trouée est superflue, en effet, on a pour toute class table $CT$ et toute paire d'expressions $e$ et $e'$ :
|
||||
|
||||
$$ \left(\forall h \; (CT,h[e])\Downarrow v \implies (CT,h[e'])\Downarrow v\right) \ssi ((CT,e)\Downarrow v \implies (CT,e')\Downarrow v)$$
|
||||
|
||||
Le sens direct se fait en particularisant à $h = [.]$ et le sens indirect se fait en appliquant les règles de réduction de congruence qui donnent
|
||||
$$\forall (e,e') \forall h\quad e\rightarrow e' \implies h[e] \rightarrow h[e']$$
|
||||
|
||||
On peut alors essayer de dire que deux expressions ont le même fonctionnement sous toute class table, c'est à dire vérifier que $\forall CT ((CT,e)\Downarrow v \implies (CT,e')\Downarrow v)$.
|
||||
|
||||
On va essayer de montrer que ce n'est pas vrai, en prouvant la chose suivante pour toute paire de formules $e$ et $e'$ qui soient cohérentes (c'est à dire $\exists CT \exists v (e,CT)\Downarrow v$, ce qui permet de s'assurer que l'on essaie pas de démentir Faux=>Faux, par exemple si $e$ vaut \fj{new A().field}):
|
||||
|
||||
$$\exists CT\quad (e,CT)\Downarrow v \land (e',CT)\not{\Downarrow} v$$
|
||||
|
||||
Hélas, ce résultat est faux, comme en témoignent les deux expressions suivantes:
|
||||
$$\fj{new Pair(new A(),new B()).fst}$$ et $$\fj{new Pair(new Pair(new A(),new B()).fst,new B()).fst}$$
|
||||
|
||||
Nous n'avons alors que trois types de classes tables: Celles qui ne compilent pas (Alors $\bot \implies \bot$), Celles où l'attribut $fst$ est donné en premier dans le constructeur de $Pair$ (Alors $e_1\Downarrow \new A()$ et $e_1\Downarrow \new A()$) et celles où l'attribut $fst$ est donné en second dans le constructeur de $Pair$ (Alors $e_1\Downarrow \new B()$ et $e_2\Downarrow \new B()$).
|
||||
|
||||
Pire encore, on a que pour toutes formules $e$ et $e'$, $\phi(e)$ et $\phi(e')$ sont équivalents en ce sens avec $\phi$ défini comme
|
||||
|
||||
$$\phi(e)=\fj{new Pair(new Pair(new A(),$e$).fst,new B()).fst}$$
|
||||
|
||||
Cela est destructeur puisque l'on obtient des équivalences entre des expressions qui sont absurdes, par exemple, si $e = \fj{new T(new T())}$ qui est une valeur, mais qu'on ne peut mettre dans aucune methode, parce que la class table ne pourrait être cohérent.
|
||||
|
||||
Nous alons donc définir la \emph{consistance} d'une liste d'expression FJ $\bar{e}$ :
|
||||
|
||||
$$\text{$e_1,e_2,\dots,e_k$ sont consistants} \ssi \exists CT \; \forall i\in \llbracket1,k\rrbracket \; \exists T \; \emptyset\vdash_{CT}e : T$$
|
||||
|
||||
\subsection{Preuve de l'inefficacité sur un ensemble d'expressions plus restreintes}
|
||||
|
||||
Nous pouvons tout de même essayer de prouver le résultat pour des expressions plus restreintes. Par exemple, des expressions qui ne sont composées que de \fj{new} et d'appels à méthode (on peut imaginer remplacer les field access par des getters).
|
||||
|
||||
Je vais maintenant expliquer comment obtenir une Class table qui prouve le théorème.
|
||||
|
||||
Nous allons créer une class table telle que la méthode $m$ de la classe $C$ aie pour type de retour $\Phi(m,C)$ qui soit un nom de classe non utilisé. Par exemple, on choisit un mot qui n'est préfixe d'aucun nom de classe utilisé (pour l'exemple \verb*|F|), on choisit aussi un délimiteur une chaine de caractères inutilisées dans les noms de méthode (pour l'exemple \verb*|@|), et on note alors le type de retour de la méthode \fj{method} dans la classe \fj{Classe} par \fj{Fmethod@Classe}. on peut alors déterminer à partir du nom de la classe d'un objet la méthode et la classe associée.
|
||||
|
||||
Ensuite, pour chaque occurence d'un appel à méthode \fj{e.m($\bar{x}$)} on détermine d'abord la classe de \fj{e}. C'est assez simple récursivement, puisque si \fj{e} est de la forme \fj{new C($\bar{x'}$)}, alors \fj{e} est de classe \fj{C}, et si \fj{e} est de la forme \fj{e'.m'($\bar{x}$)}, alors on détermine récursivement la classe \fj{C'} de \fj{e'}, puis on annonce que \fj{e} a le type $\phi(m',C')$, soit dans notre exemple $\verb*|F|m'\verb*|@|C'$.
|
||||
|
||||
Une fois que l'on a déterminé la classe de $e$, on peut ajouter à $C$ une méthode $m$ définie ainsi:
|
||||
|
||||
\begin{fjlisting}
|
||||
\method{Fm@C}{m}{Object x1,...,Object xk}{new Fm@C(this,x1,...,xk)}
|
||||
\end{fjlisting}
|
||||
|
||||
Si la classe $C$ n'existe pas et que c'est une classe de la forme \verb*|Fm@C|, alors on peut la créer ainsi.
|
||||
|
||||
\begin{fjlisting}
|
||||
\textbf{class} Fm@C \textbf{extends} Object \{\newline
|
||||
\null\qquad C obj;\newline
|
||||
\null\qquad Object x1;\newline
|
||||
\null\qquad \vdots\newline
|
||||
\null\qquad Object xk;\newline
|
||||
\null\qquad Fm@C(C obj, Object x1, \dots, Object xk)\{\newline
|
||||
\null\qquad\qquad \textbf{super()};\newline
|
||||
\null\qquad\qquad \textbf{this}.obj=obj;\newline
|
||||
\null\qquad\qquad \textbf{this}.x1=x1;\newline
|
||||
\null\qquad\qquad\vdots\newline
|
||||
\null\qquad\qquad \textbf{this}.xk=xk;\newline
|
||||
\null\qquad\}\newline
|
||||
\}
|
||||
\end{fjlisting}
|
||||
|
||||
|
||||
Appliquons maintenant à l'expression $e$ suivante :
|
||||
|
||||
\begin{center}
|
||||
\fj{new A().quoi().qui(new B().quel(new B().quoi(new A().quoi())))}
|
||||
\end{center}
|
||||
|
||||
Nous obtenons les structures de classes \textsc{Figure \ref{mRename:exampleClasses}} (dans l'ordre de lecture des applications de méthodes).
|
||||
|
||||
\ttfamily
|
||||
\begin{figure}
|
||||
\begin{tabular}{cl|rcl}
|
||||
Classe & Méthode & Types paramètres & $\rightarrow$ & Type but \\
|
||||
\hline
|
||||
A & .quoi & $\emptyset$ & $\rightarrow$ & Fquoi@A \\
|
||||
Fquoi@A & .qui & \{Fquel@B\} & $\rightarrow$ & Fqui@Fquoi@A \\
|
||||
B & .quel & \{Fquoi@B\} & $\rightarrow$ & Fquel@B \\
|
||||
B & .quoi & \{Fquoi@A\} & $\rightarrow$ & Fquoi@B \\
|
||||
A & .quoi & $\emptyset$ & $\rightarrow$ & Fquoi@A \\
|
||||
\end{tabular}
|
||||
\caption{Structures de classes obtenues par l'exemple}
|
||||
\label{mRename:exampleClasses}
|
||||
\end{figure}
|
||||
\rmfamily
|
||||
|
||||
On remarque que la première et dernière ligne sont égales. C'est normal, c'est parce que l'on appelle deux fois la même fonctions (On a une contrainte structurelle qui nous impose que ce soit la même fonction). Et puisque le programme testé est consistant, elle est appelée avec le même nombre d'arguments (possiblement des types différents, mais nous ne regardons pas le type et castons tout en \fj{Object}).
|
||||
|
||||
On obtient alors la class table \textsc{Figure \ref{mRename:createdAB} et \ref{mRename:createdF}}
|
||||
|
||||
\begin{figure}
|
||||
\begin{fjlisting}
|
||||
\fjclass{A}{}{
|
||||
\method{Fquoi@A}{quoi}{}{new Fquoi@A(this)}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\begin{fjlisting}
|
||||
\fjclass{B}{}{
|
||||
\method{Fquel@B}{quel}{Object x}{new Fquel@B(this,x)}
|
||||
\method{Fquoi@B}{quoi}{Object x}{new Fquoi@B(this,x)}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\caption{Classe A et B donnés pour l'expression exemple}
|
||||
\label{mRename:createdAB}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
\begin{fjlisting}
|
||||
\fjclass{Fquoi@A}{\attr[A]{obj}}{
|
||||
\method{Fqui@Fquoi@A}{qui}{Object x}{new Fqui@Fquoi@A(this,x)}
|
||||
}
|
||||
\fjclass{Fqui@Fquoi@A}{\attr[Fquoi@A]{obj}\attr{x}}{}
|
||||
\fjclass{Fquel@B}{\attr[B]{obj}\attr{x}}{}
|
||||
\fjclass{Fquoi@B}{\attr[B]{obj}\attr{x}}{}
|
||||
|
||||
\end{fjlisting}
|
||||
\caption{Classes artificielles pour l'expression exemple}
|
||||
\label{mRename:createdF}
|
||||
\end{figure}
|
||||
|
||||
Alors notre exemple se résout en l'objet suivant : (les \fj{new} ont été enlevés pour plus de lisibilité)
|
||||
|
||||
$$e \rightarrow^* \fj{Fqui@Fquoi@A(Fquoi@A(A),Fquel@B(B,Fquoi@B(B,Fquoi@A(A))))}$$
|
||||
|
||||
On remarque que l'on peut reconstruire la formule à partir de la valeur finale. Il suffit de remplacer \fj{new Fmethod@Class(e0,e1,...ek)} par \fj{e0.method(e1,...,ek)} puis d'appliquer récursivement sur les \fj{ei}.
|
||||
|
||||
Mais alors, étant donné deux expressions $e$ et $e'$ consistantes entre elles telles que $\forall C\; (CT,e)\Downarrow v \land (CT,e')\Downarrow v$. Alors, en particulier pour la class table que nous venons de créer, on a que les objets finaux sont égaux. Or, il est possible d'obtenir la formule qui a initié la valeur, donc les deux expressions qui n'utilisent pas les classes rajoutées, c'est à dire $e$ et $e'$ sont nécessarement égales.
|
||||
|
||||
|
||||
Nous pouvons aussi tester avec la restriction symétrique: Comment déterminer si deux programmes sont équivalents lorsqu'ils ne sont composés uniquement de \fj{new} et de \textit{field access} ?
|
||||
|
||||
Dans cet autre cas simple, on n'utiliserai aucune méthode des éventuelles Class Tables, donc deux class tables se différenciant uniquement sur leurs méthodes produitront le même résultat. La même chose pour les noms de class inutilisés, ils sont .... inutilisés et donc ne changent pas le résultat si ils apparaîssent ou disparaissent.
|
||||
|
||||
On se retrouve avec un nombre restreint de classes, il suffit de prendre la class table dans laquelle la formule est typable, de supprimer les classes inutilisées et les méthodes, puis de permuter l'ordre des attributs pour chaque classe. Il y a un nombre fini de combinaisons (encore moins si on ne considère pas les attributs non considérés), que l'on peut tester facilement (voir le contre-contre exemple du début, prouvé avec cette méthode).
|
||||
|
||||
Mais quid des cas un peu plus intermédiaires ?
|
||||
|
||||
\section{Des tests plus ciblés}
|
||||
|
||||
Une première idée afin de faire des tests plus «ciblés» est de définir arbitairement un jeu de méthodes, classes, fields, sur les quelles les programmes seront comparés.
|
||||
|
||||
\subsection{Définition des structures}
|
||||
|
||||
Nous allons tout d'abord définir une grammaire des \textit{Test sets} ou «jeux de tests» à la \textsc{Figure \ref{ts:grammaire}}. Un exemple de tests est donné à la \textsc{Figure \ref{ts:examples}} où l'on définit des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} tel qu'on puisse appeler certaines méthodes sur elles. On impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres, et on impose aussi un attribut nommé \fj{value} dans la classes RichInt.
|
||||
|
||||
Afin de valider un tests set, il faut simplement que :
|
||||
|
||||
\begin{itemize}
|
||||
\item Chaque nom de classe n'est défini que une fois par une règle de type 2 ou 3.
|
||||
\item Chaque nom de methode n'est défini que une fois par nom de classe par une règle de type 1.
|
||||
\item Les noms de classes utilisés sont définis.
|
||||
\item La relation obtenue par cloture réflexive et transitive des règles de type 4 est antisymétrique
|
||||
\end{itemize}
|
||||
|
||||
\begin{figure}
|
||||
\ttfamily
|
||||
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
|
||||
\begin{center}
|
||||
\begin{tabular}{rl}
|
||||
TS := & C : C m(bar{C}) \\
|
||||
| & C \{bar{C} bar{f}\} \\
|
||||
| & C (bar{C (? | f)}) \\
|
||||
| & C :> C
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
\end{tcolorbox}
|
||||
\rmfamily
|
||||
\caption{Grammaire des test sets}
|
||||
\label{ts:grammaire}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
\begin{fjlisting}
|
||||
Int \{\}
|
||||
|
||||
Int : Int suivant(Int)
|
||||
|
||||
Int : Int add(Int,Int)
|
||||
|
||||
\null
|
||||
|
||||
Frac(Int numerateur, Int denominateur)
|
||||
|
||||
Frac : Frac inverted()
|
||||
|
||||
Frac : Int floor()
|
||||
|
||||
\null
|
||||
|
||||
Number \{\}
|
||||
|
||||
Frac <: Number
|
||||
|
||||
Int <: Number
|
||||
|
||||
\null
|
||||
|
||||
RichInt \{Int value\}
|
||||
|
||||
RichInt : Int getInt()
|
||||
|
||||
RichInt <: Int
|
||||
|
||||
\end{fjlisting}
|
||||
\caption{Exemple de set de tests}
|
||||
\label{ts:examples}
|
||||
\end{figure}
|
||||
|
||||
Maintenant que nous avons notre grammaire, on peut définir plusieurs choses avec elles. Déjà, on va faire une relation $CT \triangleright TS$ pour dire que la class table $CT$ implémente le test set $TS$, présentée à la \textsc{Figure \ref{ts:defImpl}}
|
||||
|
||||
\begin{figure}
|
||||
\ttfamily
|
||||
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
|
||||
\begin{align}
|
||||
\infer{CT \triangleright \left[\fj{C : D m($\overline{\texttt{E}}$)}\right]}{\operatorname{mtype}_{CT}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{D}}
|
||||
\end{align}
|
||||
\begin{align}
|
||||
\infer{CT \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}{\bar{\fj{E}}\;\bar{\fj{f}} \subset \operatorname{fields}_{CT}(C)}
|
||||
\end{align}
|
||||
\begin{align}
|
||||
\infer{CT \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}{\exists \bar{\fj{f'}}\; \bar{\fj{f0}} = \bar{\fj{f}}+\bar{\fj{f'}} \land \bar{\fj{E}}\;\bar{\fj{f0}} = \operatorname{fields}_{CT}(C)}
|
||||
\end{align}
|
||||
\begin{align}
|
||||
\infer{CT \triangleright \left[\fj{C} \subclass \fj{D}\right]}{\fj{C} \subclass_{CT} \fj{D}}
|
||||
\end{align}
|
||||
\end{tcolorbox}
|
||||
\rmfamily
|
||||
\caption{Grammaire des test sets}
|
||||
\label{ts:defImpl}
|
||||
\end{figure}
|
||||
|
||||
Nous allons donc maintenant essayer de typer une expression et une class table sous un test set, dire que une expression $e$ avec sa class table associée $CT$ est «valide» dans un test set $TS$ associé, que l'on note $TS,CT \Rightarrow (\emptyset) \vdash e : T $
|
||||
|
||||
\newpage
|
||||
\bibliography{NotesStage}
|
||||
\bibliographystyle{ieeetr}
|
||||
|
||||
\end{document}
|
||||
Loading…
x
Reference in New Issue
Block a user