Corrections suite aux indications de Clement.
This commit is contained in:
parent
c91bc559b9
commit
b880b5f59a
GPG Key ID:
7054D5D6A90F084F
3
.gitignore
vendored
3
.gitignore
vendored
@ -5,3 +5,6 @@ NotesStage.pdf
|
||||
*.synctex.gz
|
||||
*.bbl
|
||||
*.blg
|
||||
*.fdb_latexmk
|
||||
*.fls
|
||||
*.out
|
||||
|
||||
3
Makefile
3
Makefile
@ -1,8 +1,7 @@
|
||||
all: NotesStage.pdf
|
||||
|
||||
NotesStage.pdf:
|
||||
pdflatex NotesStage.tex
|
||||
pdflatex NotesStage.tex
|
||||
latexmk -pdf NotesStage.tex
|
||||
|
||||
clean:
|
||||
git clean -Xf
|
||||
|
||||
@ -50,4 +50,22 @@
|
||||
PDF = {https://hal.inria.fr/inria-00432540/file/TCS-60.pdf},
|
||||
HAL_ID = {inria-00432540},
|
||||
HAL_VERSION = {v1},
|
||||
}
|
||||
@InProceedings{kuci_et_al:cocoTypecheck,
|
||||
author = {Edlira Kuci and Sebastian Erdweg and Oliver Bracevac and Andi Bejleri and Mira Mezini},
|
||||
title = {{A Co-contextual Type Checker for Featherweight Java }},
|
||||
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
|
||||
pages = {18:1--18:26},
|
||||
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
|
||||
ISBN = {978-3-95977-035-4},
|
||||
ISSN = {1868-8969},
|
||||
year = {2017},
|
||||
volume = {74},
|
||||
editor = {Peter M{\"u}ller},
|
||||
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
|
||||
address = {Dagstuhl, Germany},
|
||||
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7262},
|
||||
URN = {urn:nbn:de:0030-drops-72628},
|
||||
doi = {10.4230/LIPIcs.ECOOP.2017.18},
|
||||
annote = {Keywords: type checking, co-contextual, constraints, class table, Featherweight Java}
|
||||
}
|
||||
291
NotesStage.tex
291
NotesStage.tex
@ -1,6 +1,16 @@
|
||||
\documentclass[10pt,a4paper,draft]{article}
|
||||
% !TeX spellcheck = fr_FR
|
||||
\documentclass[10pt,a4paper]{article}
|
||||
|
||||
% Loading packages
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage{hyperref}
|
||||
\hypersetup{
|
||||
colorlinks=true,
|
||||
linkcolor=blue,
|
||||
filecolor=magenta,
|
||||
urlcolor=cyan
|
||||
}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amssymb}
|
||||
\usepackage{bbm}
|
||||
@ -17,9 +27,12 @@
|
||||
\usepackage{tcolorbox}
|
||||
\usepackage{mdframed}
|
||||
\usepackage{proof}
|
||||
|
||||
\usepackage{csquotes}
|
||||
\usepackage[lighttt]{lmodern}
|
||||
\usetikzlibrary{shapes.geometric}
|
||||
|
||||
% Macros caractères globales
|
||||
\newcommand{\pgrph}{\P}
|
||||
\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}}
|
||||
\renewcommand{\P}{\mathbb{P}}
|
||||
@ -29,52 +42,55 @@
|
||||
\newcommand{\littleO}{o}
|
||||
\newcommand{\bigO}{\mathcal{O}}
|
||||
\newcommand{\longdash}{\:\textrm{---}\:}
|
||||
\newcommand{\methprec}[1]{\prec\mkern-8mu\left[\fj{#1}\right]}
|
||||
\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]}
|
||||
\newcommand\bracket[1]{\right[#1\left]}
|
||||
\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
|
||||
|
||||
% Création des environnement globaux
|
||||
\newtheorem{theorem}{Théorème}
|
||||
\newtheorem{definition}{Definition}
|
||||
\newtheorem{property}{Propriété}
|
||||
\addto\extrasfrench{%
|
||||
\renewcommand{\figureautorefname}{\textsc{Figure}}%
|
||||
}
|
||||
|
||||
% Commandes logiques globales
|
||||
\newcommand{\ifnullthenelse}[3]{
|
||||
\ifnum\value{#1}=0
|
||||
#2
|
||||
\else
|
||||
#3
|
||||
\fi
|
||||
}
|
||||
|
||||
%%% Commande \newtag permettant de changer le label d'une equation
|
||||
\makeatletter
|
||||
\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}}
|
||||
\makeatother
|
||||
|
||||
% Macros caractères spécifiques au document
|
||||
\newcommand{\methprec}[1]{\prec\mkern-8mu\left[\fj{#1}\right]}
|
||||
\DeclareMathOperator{\varnull}{varnull}
|
||||
\DeclareMathOperator{\nextop}{next}
|
||||
\DeclareMathOperator{\new}{\text{\textbf{new}}}
|
||||
\DeclareMathOperator{\CT}{CT}
|
||||
\DeclareRobustCommand{\leftsarrow}{\text{\reflectbox{$\;\rightarrow^*$}}}
|
||||
\let\rbar\bar
|
||||
\let\bar\overline
|
||||
\newcommand\subclass{<:}
|
||||
|
||||
\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
|
||||
|
||||
\newtheorem{theorem}{Théorème}
|
||||
\newtheorem{definition}{Definition}
|
||||
\newtheorem{property}{Propriété}
|
||||
|
||||
\tcbuselibrary{fitting}
|
||||
% Création des environnements spécifiques au document
|
||||
|
||||
%%% Blocs colorés pour le code FeatherweightJava
|
||||
\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}
|
||||
\newtcbox{\fjind}{nobeforeafter,tcbox raise base, rounded corners=all, boxsep=0pt,left=1pt,right=1pt,top=1pt,bottom=1pt,boxrule=0pt,colback=white!52!orange}
|
||||
|
||||
\newenvironment{fjlisting}[1][]
|
||||
{
|
||||
%\begin{center}
|
||||
{
|
||||
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!96!black,#1]
|
||||
\ttfamily
|
||||
}{
|
||||
\end{tcolorbox}
|
||||
%\end{center}
|
||||
}
|
||||
\newcommand{\ifnullthenelse}[3]{
|
||||
\ifnum\value{#1}=0
|
||||
#2
|
||||
\else
|
||||
#3
|
||||
\fi
|
||||
}{
|
||||
\end{tcolorbox}
|
||||
}
|
||||
|
||||
% Langage Featherweight Java
|
||||
\makeatletter
|
||||
\newcommand*\idstyle{%
|
||||
\expandafter\id@style\the\lst@token\relax
|
||||
@ -87,15 +103,18 @@
|
||||
\fi
|
||||
}
|
||||
\makeatother
|
||||
|
||||
\lstdefinelanguage{FeatherweightJava}{
|
||||
keywords = {new, this},
|
||||
basicstyle=\ttfamily,
|
||||
identifierstyle=\idstyle,
|
||||
mathescape=true
|
||||
mathescape=true,
|
||||
escapechar=\$
|
||||
}
|
||||
\newcommand{\fj}[1]{\text{\textnormal{\lstinline[language=FeatherweightJava,mathescape=true]|#1|}}}
|
||||
\newcommand{\fj}[1]{\text{\textnormal{\lstinline[language=FeatherweightJava]|#1|}}}
|
||||
|
||||
|
||||
% Définition des macros pour l'écriture des trucs Featherweight Java
|
||||
\newcommand\fjattr{\GenericWarning{$\backslash$ fjattr doit être utilisé dans une fjclass}}
|
||||
\newcounter{fjargcount}
|
||||
\newcommand{\fjparamattributes}[2][Object]{
|
||||
\null\qquad #1 #2;\newline
|
||||
@ -108,9 +127,9 @@
|
||||
\newcommand{\fjparamconstassign}[2][Object]{
|
||||
\null\qquad\qquad \textbf{this}.#2 = #2;\newline
|
||||
}
|
||||
\newcommand{\method}[4]{
|
||||
\newcommand{\fjmethod}[4]{
|
||||
\null\qquad #1 #2(#3)\{\newline
|
||||
\null\qquad\qquad \textbf{return} \lstinline[language=Java]{#4};\newline
|
||||
\null\qquad\qquad \textbf{return} \lstinline[language=FeatherweightJava]{#4};\newline
|
||||
\null\qquad\}\newline
|
||||
}
|
||||
|
||||
@ -119,28 +138,30 @@
|
||||
}
|
||||
|
||||
% 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
|
||||
% Second argument: \fjattr{x}[Object] \fjattr{attr}[A]
|
||||
% Troisième argument \fjmethod{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
|
||||
\let\fjattr\fjparamattributes
|
||||
#3
|
||||
% Constructeur
|
||||
\let\attr\fjparamconstparameters
|
||||
\let\fjattr\fjparamconstparameters
|
||||
\setcounter{fjargcount}{0}
|
||||
\null\qquad #2(\ifx&\else $#3$\fi) \{\newline
|
||||
\null\qquad\qquad \textbf{super}();\newline
|
||||
\let\attr\fjparamconstassign%
|
||||
\let\fjattr\fjparamconstassign%
|
||||
#3
|
||||
\null\qquad\}\\
|
||||
% Méthodes
|
||||
#4
|
||||
\}\newline
|
||||
\}
|
||||
}
|
||||
|
||||
\title{Notes de Stage}
|
||||
\title{Vers la définition d'un préordre sur les programmes FeatherweightJava
|
||||
\\[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}
|
||||
|
||||
\begin{document}
|
||||
@ -158,15 +179,15 @@
|
||||
\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.
|
||||
Donc $e$ est la grammaire des expressions, $L$ la grammaire des classes, $\overline{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.
|
||||
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 \textit{body} d'une fonction \fj{main} d'un programmme Java). Nous allons donc considérer qu'un programme FeatherweightJava $P$ est un couple $(\overline{L},e)$, et l'on notera $\CT(P) = \overline{L}$ et $e_P = e$ lorsque nous manipulerons plusieurs programmes.
|
||||
|
||||
On note la gramaire à un trou $h$ :
|
||||
$$h := \fj{x} | \fj{[.]} | \fj{h.f} | \fj{h.m(}\bar{\fj{e}}\fj{)} | \fj{e.m(}\bar{\fj{e}}\fj{,h,}\bar{\fj{e}}\fj{)} | \fj{new C(}\bar{\fj{e}}\fj{,h,}\bar{\fj{e}}) | \fj{(C) h} $$
|
||||
$$h := \fj{x} | \fj{[.]} | \fj{h.f} | \fj{h.m(}\overline{\fj{e}}\fj{)} | \fj{e.m(}\overline{\fj{e}}\fj{,h,}\overline{\fj{e}}\fj{)} | \fj{new C(}\overline{\fj{e}}\fj{,h,}\overline{\fj{e}}) | \fj{(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 $$
|
||||
$$\tilde{h} := x | [.] | \tilde{h}.f | \tilde{h}.m(\overline{\tilde{h}}) | \new C(\overline{\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:
|
||||
|
||||
@ -174,9 +195,9 @@
|
||||
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})\\
|
||||
(h.m(\overline{e}))[g] &= h[g].m(\overline{e})\\
|
||||
(e.m(\overline{e},h,\overline{e}))[g] &= e.m(\overline{e},h[g],\overline{e})\\
|
||||
(\new C(\overline{e},h,\overline{e}))[g] &= \new C(\overline{e},h[g],\overline{e})\\
|
||||
((C) h)[g] &= (C) h[g]
|
||||
\end{align*}
|
||||
|
||||
@ -186,46 +207,51 @@
|
||||
|
||||
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])$
|
||||
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.
|
||||
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 \textit{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$.
|
||||
Si la \textit{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}
|
||||
|
||||
\begin{fjlisting}
|
||||
|
||||
\fjclass{Pair}{
|
||||
\attr{fst}
|
||||
\attr{snd}
|
||||
\fjattr{fst}
|
||||
\fjattr{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}.
|
||||
Alors si on considère le contexte suivant : \[C = \fj{new Pair(e,[.]).fst}\]
|
||||
|
||||
On aura pour toute expression \fj{e} : \[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.
|
||||
Le théorème se prouve en construisant des expressions qui dépendent explicitement de la structure des classes. Par exemple, \fj{new A()} ne se résout en une valeur seulement si la \textit{class table} contient une classe \fj{A} sans attributs. On peut aussi par exemple imposer le type des attributs de \fj{C} ainsi que l'existence d'une méthode \fj{C.m} prenant un argument de type \fj{A} avec l'expression suivante : \[\fj{new C(new A(), new B()).m(new A())}\]
|
||||
|
||||
\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{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 \enquote{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 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 \enquote{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 autre solution} pourrait être de comparer uniquement avec des contextes qui \enquote{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$.
|
||||
Un contexte est une class table $\overline{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)$.
|
||||
Alors $C[P] = (\CT(P) + \overline{L'}, h[\overline{L'}/\overline{L}][e_P])$ où $\overline{L'}$ est une \textit{class table} $\alpha$-convertible en $\overline{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é.
|
||||
|
||||
@ -234,23 +260,23 @@
|
||||
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$.
|
||||
Un contexte est une class table $\overline{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:
|
||||
Alors $C[P] = (\CT(P) + \overline{L}' + Main'', e_C[CT'/CT][Main''/Main])$ où $\overline{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}
|
||||
\fjmethod{Object}{main}{Object $\overline{x}$}{e}
|
||||
}
|
||||
\end{fjlisting}
|
||||
|
||||
où $\bar{x}$ est l'ensemble des variable libres de $e_P$.
|
||||
où $\overline{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])})$$
|
||||
$C$ = $\overline{L}$ et $\overline{e_C}$ interprété en
|
||||
$$C[P] = (\CT(P) + \overline{L}' + Main'', \new Main().main(\overline{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.
|
||||
@ -259,44 +285,44 @@
|
||||
|
||||
$$ 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:
|
||||
On peut ainsi utiliser la méthode du contexte pour créer le préordre suivant 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$$
|
||||
\[ P \prec Q \iff \left|\begin{array}{l}\CT(P) \prec \CT(Q) \\ \forall h (\CT(P),h[e_P])\Downarrow v \implies (\CT(Q), h[e_Q])\Downarrow v\end{array}\right.\]
|
||||
|
||||
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$.
|
||||
Un contexte $C$ est alors une CT $\overline{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$.
|
||||
L'interpretation est alors $C[P] = (CT(C),h[e_P])$ si $\CT(P) \prec \CT(C)$. On dit alors que $C$ convient à $P$, noté $C \triangleleft 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)$$
|
||||
$$P\prec Q \iff \forall C (C \triangleleft P\text{ et }C \triangleleft 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{minipage}{.49\textwidth}
|
||||
\begin{fjlisting}
|
||||
\fjclass{A}{}{}
|
||||
\fjclass{B}{}{}
|
||||
\fjclass{Get}{
|
||||
\attr[A]{a}
|
||||
\attr[B]{b}
|
||||
\fjattr[A]{a}
|
||||
\fjattr[B]{b}
|
||||
}{
|
||||
\method{Object}{get}{}{this.a}
|
||||
\fjmethod{Object}{get}{}{this.a}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\end{minipage}
|
||||
\begin{minipage}{.5\textwidth}
|
||||
\begin{minipage}{.49\textwidth}
|
||||
\begin{fjlisting}
|
||||
\fjclass{A}{}{}
|
||||
\fjclass{B}{}{}
|
||||
\fjclass{Get}{
|
||||
\attr[A]{a}
|
||||
\attr[B]{b}
|
||||
\fjattr[A]{a}
|
||||
\fjattr[B]{b}
|
||||
}{
|
||||
\method{Object}{get}{}{this.b}
|
||||
\fjmethod{Object}{get}{}{this.b}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\end{minipage}
|
||||
@ -358,7 +384,7 @@
|
||||
|
||||
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}$ :
|
||||
Nous alons donc définir la \emph{consistance} d'une liste d'expression FJ $\overline{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$$
|
||||
|
||||
@ -370,12 +396,14 @@
|
||||
|
||||
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'$.
|
||||
Ensuite, pour chaque occurence d'un appel à méthode \fj{e.m($\overline{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($\overline{x'}$)}, alors \fj{e} est de classe \fj{C}, et si \fj{e} est de la forme \fj{e'.m'($\overline{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)}
|
||||
Fm@C m(Object x1,...,Object xk)\{\newline
|
||||
\null\quad\textbf{return} new Fm@C(this,x1,...,xk);\newline
|
||||
\}
|
||||
\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.
|
||||
@ -403,7 +431,7 @@
|
||||
\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).
|
||||
Nous obtenons les structures de classes \autoref{mRename:exampleClasses} (dans l'ordre de lecture des applications de méthodes).
|
||||
|
||||
\ttfamily
|
||||
\begin{figure}
|
||||
@ -423,18 +451,18 @@
|
||||
|
||||
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}}
|
||||
On obtient alors la class table \autoref{mRename:createdAB} et \autoref{mRename:createdF}
|
||||
|
||||
\begin{figure}
|
||||
\begin{fjlisting}
|
||||
\fjclass{A}{}{
|
||||
\method{Fquoi@A}{quoi}{}{new Fquoi@A(this)}
|
||||
\fjmethod{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)}
|
||||
\fjmethod{Fquel@B}{quel}{Object x}{new Fquel@B(this,x)}
|
||||
\fjmethod{Fquoi@B}{quoi}{Object x}{new Fquoi@B(this,x)}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\caption{Classe A et B donnés pour l'expression exemple}
|
||||
@ -443,12 +471,12 @@
|
||||
|
||||
\begin{figure}
|
||||
\begin{fjlisting}
|
||||
\fjclass{Fquoi@A}{\attr[A]{obj}}{
|
||||
\method{Fqui@Fquoi@A}{qui}{Object x}{new Fqui@Fquoi@A(this,x)}
|
||||
\fjclass{Fquoi@A}{\fjattr[A]{obj}}{
|
||||
\fjmethod{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}}{}
|
||||
\fjclass{Fqui@Fquoi@A}{\fjattr[Fquoi@A]{obj}\fjattr{x}}{}
|
||||
\fjclass{Fquel@B}{\fjattr[B]{obj}\fjattr{x}}{}
|
||||
\fjclass{Fquoi@B}{\fjattr[B]{obj}\fjattr{x}}{}
|
||||
|
||||
\end{fjlisting}
|
||||
\caption{Classes artificielles pour l'expression exemple}
|
||||
@ -474,11 +502,11 @@
|
||||
|
||||
\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.
|
||||
Une première idée afin de faire des tests plus \enquote{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{ti:grammaire}}. Un exemple de tests est donné à la \textsc{Figure \ref{ti: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.
|
||||
Nous allons tout d'abord définir une grammaire des \textit{Test interfaces} ou \enquote{interfaces de tests} à la \autoref{ti:grammaire}. Un exemple de tests est donné à la \autoref{ti: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.
|
||||
|
||||
\begin{figure}
|
||||
\ttfamily
|
||||
@ -537,20 +565,20 @@
|
||||
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 \ref{tsg:attributes} et \ref{tsg:constructor}.
|
||||
\item Chaque nom de methode n'est défini que une fois par nom de classe par une règle de type \ref{tsg:method}.
|
||||
\item Chaque nom de classe est défini au plus une fois par une règle de type \ref{tsg:attributes} et \ref{tsg:constructor}.
|
||||
\item Chaque nom de methode est défini au plus une fois par nom de classe par une règle de type \ref{tsg:method}.
|
||||
\item Les noms de classes utilisés sont définis.
|
||||
\end{itemize}
|
||||
|
||||
On pourrait se questionner sur la structure donnée aux règles \ref{tsg:attributes} et \ref{tsg:constructor}. La différence fondamentale entre les deux est que la première n'autorise pas à appeler \fj{new C(...)} alors que la seconde l'autorise. La première autorise seulement l'accès aux champs de la classe. On pourrait alors critiquer que cette façon de définir les règles ne permet pas d'autoriser la création d'un objet avec \fj{new} et d'autoriser certains \textit{field access} sans en imposer l'ordre. Pourtant, autoriser ces deux constructions impose que deux \textit{class tables} qui seraient équivalentes auraient le champ à la même position. Par exemple, on peut construire une expression simple \fj{new C(new P1(), new P2(), new P3(), ...).field} où \fj{P1}, \fj{P2}, \fj{P3} sont des classes créées pour l'occasion, qui ont des paramètes cohérents, etc… Alors cette expression se réduira en la même valeur dans deux \textit{class table} si et seulement si l'attribut \fj{field} est assigné au même indice dans le constructeur de \fj{C} dans les deux class tables.
|
||||
|
||||
La troisième règle permet d'éviter des définitions «implicites» de classes, en suivant la convention suivie par la première définition du Featherweight Java \cite{fjdef}. On peut sinon ajouter la règle \fj{A\{\}} pour chaque nom de classe utilisé sans être défini.
|
||||
La troisième règle permet d'éviter des définitions \enquote{implicites} de classes, en suivant la convention suivie par la première définition du Featherweight Java \cite{fjdef}. On peut sinon ajouter la règle \fj{A\{\}} pour chaque nom de classe utilisé sans être défini.
|
||||
|
||||
Nous allons aussi rajouter trois règles, qui ne sont pas strictement nécessaires, mais qui permettent de restreindre les tests sets aux tests sets «intéréssants», en enlevant certaines contraintes qui feraient apparaître des méthodes ou objets inutilisables.
|
||||
Nous allons aussi rajouter trois règles, qui ne sont pas strictement nécessaires, mais qui permettent de restreindre les tests sets aux tests sets \enquote{intéréssants}, en enlevant certaines contraintes qui feraient apparaître des méthodes ou objets inutilisables.
|
||||
|
||||
\begin{itemize}
|
||||
\item La relation obtenue par cloture réflexive et transitive des règles de type \ref{tsg:cast} est un bon ordre (en ajoutant la classe virtuelle \fj{Object})
|
||||
\item Dans les ocurrences des règles \ref{tsg:attributes} et \ref{tsg:constructor}, la relation «est le type d'un attribut» induit un bon ordre.
|
||||
\item Dans les ocurrences des règles \ref{tsg:attributes} et \ref{tsg:constructor}, la relation \enquote{est le type d'un attribut} induit un bon ordre.
|
||||
\item Pour chaque règle \ref{tsg:cast} \fj{C :> B}, alors, la propriété adéquate est vérifiée, suivant les règles qui ont défini \fj{C} et \fj{B} selon le tableau suivant:
|
||||
\vspace{1ex}
|
||||
\begin{tabular}{c|c|c|}
|
||||
@ -564,7 +592,7 @@
|
||||
|
||||
La troisième règle force les contraintes sur les types et noms des attributs à être cohérentes.
|
||||
|
||||
On aimerai dire qu'il existe toujours au moins une \textit{class table} qui implémente une \textit{test interface} qui respecte toutes ces règles, mais hélas, ce n'est pas vrai, si l'on considère de manière naïve la relation «est le type d'un attribut» induit par la règle 2, voir troisième exemple de la \textsc{Figure \ref{ti:examplesfaux}}
|
||||
On aimerai dire qu'il existe toujours au moins une \textit{class table} qui implémente une \textit{test interface} qui respecte toutes ces règles, mais hélas, ce n'est pas vrai, si l'on considère de manière naïve la relation \enquote{est le type d'un attribut} induit par la règle 2, voir troisième exemple de la \autoref{ti:examplesfaux}
|
||||
|
||||
Cependant, on peut toujours (si la première et la troisième règle sont vérifiées) créer une class table bidon qui ne compile jamais. Pour cela, il suffit d'implémenter naïvement chaque class, sauf que nous remplaçons chaque occurence de \fj{extends Object} par \fj{extends SObject} (où \fj{SObject} est un nom de classe inutilisé). On crée la classe SObject avec un constructeur ne prenant pas de paramètre. Alors, on peut implémenter n'importe quelle méthode du type $\overline{\fj{M}} \rightarrow \fj{T}$ par l'expression \fj{(T) new SObject()}. L'expression est bien typable en \fj{T} puisque SObject est une superclasse de tous les types (sauf Object, auquel cas renvoyer simplement \fj{new SObject()}). Mais bien sûr, ces méthodes ne pourrons jamais renvoyer une valeur car le cast sera toujours impossible.
|
||||
|
||||
@ -607,7 +635,7 @@
|
||||
\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 TI$ pour dire que la class table $CT$ implémente la test interface $TI$, présentée à la \textsc{Figure \ref{ti:defImpl}}. L'implémentation est la plus tolérante possible quant au typage notamment des méthodes, car on ne veut pas comparer les \textit{class tables} sur leur typage, mais bien sur leur fonctionnement, le typage reste un garde-fou qui nous empêche de tester tout et n'importe quoi et d'obtenir une relation inexploitable. Typiquement, les deux \textit{class tables} présentées \textsc{Figure \ref{ti:exempletolerance}} implémenteront toutes deux la test interface jointe, et seront donc équivalentes.
|
||||
Maintenant que nous avons notre grammaire, on peut définir plusieurs choses avec elles. Déjà, on va faire une relation $CT \triangleright TI$ pour dire que la class table $CT$ implémente la test interface $TI$, présentée à la \autoref{ti:defImpl}. L'implémentation est la plus tolérante possible quant au typage notamment des méthodes, car on ne veut pas comparer les \textit{class tables} sur leur typage, mais bien sur leur fonctionnement, le typage reste un garde-fou qui nous empêche de tester tout et n'importe quoi et d'obtenir une relation inexploitable. Typiquement, les deux \textit{class tables} présentées \autoref{ti:exempletolerance} implémenteront toutes deux la test interface jointe, et seront donc équivalentes.
|
||||
|
||||
\begin{figure}
|
||||
\ttfamily
|
||||
@ -616,10 +644,10 @@
|
||||
\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)}
|
||||
\infer{CT \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}{\overline{\fj{E}}\;\overline{\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)}
|
||||
\infer{CT \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}{\exists \overline{\fj{f'}}\; \overline{\fj{f0}} = \overline{\fj{f}}+\overline{\fj{f'}} \land \overline{\fj{E}}\;\overline{\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}}
|
||||
@ -644,17 +672,21 @@
|
||||
\begin{multicols}{2}
|
||||
\begin{fjlisting}[width=.48\textwidth]
|
||||
\fjclass{A}{}{}
|
||||
|
||||
\fjclass[A]{B}{}{}
|
||||
|
||||
\fjclass{Static}{}{
|
||||
\method{A}{get}{}{new B();}
|
||||
\fjmethod{A}{get}{}{new B();}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\columnbreak
|
||||
\begin{fjlisting}[width=.48\textwidth]
|
||||
\fjclass{A}{}{}
|
||||
|
||||
\fjclass[A]{B}{}{}
|
||||
|
||||
\fjclass{Static}{}{
|
||||
\method{B}{get}{}{new B();}
|
||||
\fjmethod{B}{get}{}{new B();}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\end{multicols}
|
||||
@ -664,9 +696,9 @@
|
||||
\caption{Exemple de classes justifiant la tolérance dans la définition de $\triangleright$}
|
||||
\end{figure}
|
||||
|
||||
Nous allons donc maintenant essayer de typer une expression et une class table sous une test interface, dire que une expression $e$ avec sa class table associée $CT$ est «valide» dans un test interface $TI$ associé, que l'on note $TI,CT \Vdash e : T$ (pour bien différencier de la règle de typage de Featherweight Java, notée $\vdash$).
|
||||
Nous allons donc maintenant essayer de typer une expression et une class table sous une test interface, dire que une expression $e$ avec sa class table associée $CT$ est \enquote{valide} dans un test interface $TI$ associé, que l'on note $TI,CT \Vdash e : T$ (pour bien différencier de la règle de typage de Featherweight Java, notée $\vdash$).
|
||||
|
||||
La présence d'une \textit{class table} associée à l'expression est nécessaire car il existe deux \textit{class tables} implémentant la même \textit{test interfaces} qui ne sont pas différenciables par des expressions seules, mais qui le sont lorsque l'on ajoute un class table (voir exemple \textsc{Figure \ref{ti:exempleneedct}}).
|
||||
La présence d'une \textit{class table} associée à l'expression est nécessaire car il existe deux \textit{class tables} implémentant la même \textit{test interfaces} qui ne sont pas différenciables par des expressions seules, mais qui le sont lorsque l'on ajoute un class table (voir exemple \autoref{ti:exempleneedct}).
|
||||
|
||||
\begin{figure}
|
||||
|
||||
@ -681,14 +713,14 @@
|
||||
\begin{fjlisting}[width=.48\textwidth]
|
||||
\fjclass{B}{}{}
|
||||
\fjclass{Static}{}{
|
||||
\method{B}{get}{B in}{in}
|
||||
\fjmethod{B}{get}{B in}{in}
|
||||
}
|
||||
\end{fjlisting}
|
||||
|
||||
\begin{fjlisting}[width=.48\textwidth]
|
||||
\fjclass{B}{}{}
|
||||
\fjclass{Static}{}{
|
||||
\method{B}{get}{B in}{new B()}
|
||||
\fjmethod{B}{get}{B in}{new B()}
|
||||
}
|
||||
\end{fjlisting}
|
||||
|
||||
@ -700,10 +732,10 @@
|
||||
|
||||
|
||||
\label{ti:exempleneedct}
|
||||
\caption{Exemple de class tables différentiables uniquement avec une class table}
|
||||
\caption{Exemple montrant l'utilité de la \textit{class table} de test}
|
||||
\end{figure}
|
||||
|
||||
Les règles de typage sont obtenues en modifiant quelque peu les règles de typage de Featherweight java. La première étape est de définir les deux applications \textit{mtype} à partir des règles de type 1 et des déclarations de méthodes, et \textit{fields} qui s'obtient à partir des règles deux et trois et des champs présents dans la \textit{class table}. On rajoute enfin une application $\operatorname{construct(C)}$ qui est défini avec deux règles, l'une à partir de la règle trois et l'autre à partir des constructeurs réels (voir \textsc{Figure \ref{ti:defconstruct}}).
|
||||
Les règles de typage sont obtenues en modifiant quelque peu les règles de typage de Featherweight java. La première étape est de définir les deux applications \textit{mtype} à partir des règles de type 1 et des déclarations de méthodes, et \textit{fields} qui s'obtient à partir des règles deux et trois et des champs présents dans la \textit{class table}. On rajoute enfin une application $\operatorname{construct(C)}$ qui est défini avec deux règles, l'une à partir de la règle trois et l'autre à partir des constructeurs réels (voir \autoref{ti:defconstruct}).
|
||||
|
||||
\begin{figure}
|
||||
\ttfamily
|
||||
@ -720,7 +752,7 @@
|
||||
\label{ti:defconstruct}
|
||||
\end{figure}
|
||||
|
||||
Nous pouvons alors définir la relation de typage d'une expression sous une \textit{class table} et une \textit{test interface} avec des règles d'inférence présentées \textsc{Figure \ref{ti:deftyp}}. On ajoute aussi toutes les règles de typage d'expression présentées dans la définition du FJ Java \cite[p. 404]{fjdef}, en enlevant la règle \textsc{T-SCast} qui n'ajoute pas grand chose ...
|
||||
Nous pouvons alors définir la relation de typage d'une expression sous une \textit{class table} et une \textit{test interface} avec des règles d'inférence présentées \autoref{ti:deftyp}. On ajoute aussi toutes les règles de typage d'expression présentées dans la définition du FJ Java \cite[p. 404]{fjdef}, en enlevant la règle \textsc{T-SCast} qui n'ajoute pas grand chose ...
|
||||
|
||||
\begin{figure}
|
||||
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
|
||||
@ -763,7 +795,7 @@
|
||||
|
||||
Alors il existe \fj{C} tel que $CT \oplus CT_t \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$.
|
||||
|
||||
Cette dernière condition est nécessaire à cause de la tolérance de l'opérateur $\triangleright$, comme est démontré par l'exemple \textsc{Figure \ref{ti:exempletolth}}.
|
||||
Cette dernière condition est nécessaire à cause de la tolérance de l'opérateur $\triangleright$, comme est démontré par l'exemple \autoref{ti:exempletolth}.
|
||||
|
||||
\begin{figure}
|
||||
\begin{fjlisting}
|
||||
@ -777,7 +809,7 @@
|
||||
\begin{fjlisting}
|
||||
\fjclass{E}{}{}
|
||||
\fjclass[E]{F}{}{}
|
||||
\fjclass{F}{}{\method{F}{m}{}{new F()}}
|
||||
\fjclass{F}{}{\fjmethod{F}{m}{}{new F()}}
|
||||
\end{fjlisting}
|
||||
|
||||
$$e = \fj{new D().m()}$$
|
||||
@ -812,7 +844,8 @@
|
||||
$$CT_1 \prec_{TS} CT_2 \iff \forall \left[\fj{Class : D meth(}\overline{\fj{E}}\fj{)}\right] \in TI \quad CT_1 \methprec{Class.meth} CT_2$$
|
||||
\end{theorem}
|
||||
|
||||
\subsubsection{Ajout de \fj{null} à Featherweight Java}
|
||||
\setcounter{subsection}{-1}
|
||||
\subsection{Ajout de \texorpdfstring{\fj{null}}{null} à Featherweight Java}
|
||||
|
||||
%TODO décrire le choix de l'implémentation de null typé
|
||||
|
||||
@ -848,7 +881,7 @@
|
||||
|
||||
Enfin, nous avons $e_2 \rightarrow e'$ car il suffit de réduire séquentiellement chaque nœud marqué dans $e_2$ par la même opération que pour $e \rightarrow e_1$, et nous obtenons par définition e'.
|
||||
|
||||
\subsubsection{Obtention des ensembles de valeurs $V$}
|
||||
\subsubsection{Obtention des ensembles de valeurs \texorpdfstring{$V$}{V}}
|
||||
|
||||
Pour créer l'ensemble de valeurs, nous allons nous restreindre à une seule \textit{class table} (la relation de réduction est donc simplement notée $\rightarrow$) et une seule expression $e \in \overline{d}$.
|
||||
|
||||
@ -932,14 +965,14 @@
|
||||
|
||||
\subsection{Exemples montrant l'inutilité de l'équivalence sur les méthodes}
|
||||
\begin{fjlisting}
|
||||
\fjclass{IList}{\attr[IList]{next} \attr[Object]{obj}}{}
|
||||
\fjclass{IList}{\fjattr[IList]{next} \fjattr[Object]{obj}}{}
|
||||
\fjclass{Static}{}{
|
||||
\null\qquad IList gen()\{\newline
|
||||
\fjind{$CT_1 - CT_1'$}\null\qquad \textbf{return} \lstinline[language=Java]{new IList(0,new IList(1,gen()))};\newline
|
||||
\fjind{$CT_2 - CT_2'$}\null\qquad \textbf{return} \lstinline[language=Java]{new IList(0,gen())};\newline
|
||||
\null\qquad\}\newline
|
||||
|
||||
\method{Object}{evilNext}{Object x}{x.next}
|
||||
\fjmethod{Object}{evilNext}{Object x}{x.next}
|
||||
}
|
||||
\end{fjlisting}
|
||||
|
||||
@ -967,18 +1000,18 @@
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
|
||||
On peut montrer les «non» en utilisant les expressions $e=\fj{new Static().gen().next.obj}$ et $e'=\fj{new Static().evilNext(new Static().get()).obj}$.
|
||||
On peut montrer les \enquote{non} en utilisant les expressions $e=\fj{new Static().gen().next.obj}$ et $e'=\fj{new Static().evilNext(new Static().get()).obj}$.
|
||||
|
||||
Aussi, dans ces exemples, les \textit{class tables} $CT_1/CT_2$ et $CT_1'/CT_2'$ sont équivalents sous l'angle de toutes les méthodes des \textit{test interfaces}. Et pourtant ne sont pas équivalentes sous certaines.
|
||||
|
||||
On pourrait vouloir palier ce problème en comparant les méthodes sur les valeurs «infinies» qu'elles produisent, mais de la même façon, les \textit{class tables} ne sont alors jamais équivalentes sous l'angle de \fj{Static.get}, mais elles sont parfois équivalentes (comme sous $TI_1$).
|
||||
On pourrait vouloir palier ce problème en comparant les méthodes sur les valeurs \enquote{infinies} qu'elles produisent, mais de la même façon, les \textit{class tables} ne sont alors jamais équivalentes sous l'angle de \fj{Static.get}, mais elles sont parfois équivalentes (comme sous $TI_1$).
|
||||
|
||||
L'exemple $TI_2$ et $TI_2'$ nous indique qu'on ne peut pas se contenter de comparer les valeurs de sortie sur les fields laissés apparents par la test interface.
|
||||
\subsection{Encore quelques critiques sur la définition de l'équivalence de classes}
|
||||
|
||||
Je vais encore apporter une critique à la définition de l'équivalence de classes avec les Test Interfaces. Ce ne sont pas ces dernières le problème, mais plutôt la définition du préordre qui en suit. En effet, cette définition «teste» les class table sur toutes les valeurs possibles, et y impose donc des contraintes. Ainsi, deux objets au nom de classes différent seront nécessairement distincts.
|
||||
Je vais encore apporter une critique à la définition de l'équivalence de classes avec les Test Interfaces. Ce ne sont pas ces dernières le problème, mais plutôt la définition du préordre qui en suit. En effet, cette définition \enquote{teste} les class table sur toutes les valeurs possibles, et y impose donc des contraintes. Ainsi, deux objets au nom de classes différent seront nécessairement distincts.
|
||||
|
||||
En effet, les deux class tables données \textsc{Figure \ref{classeq:ex}} ne sont pas équivalentes pour la \textit{test interface} donnée (l'expression \fj{new Static().true()}) premet de les distinguer, car \fj{new Bool()} est différent de \fj{new Other()}.
|
||||
En effet, les deux class tables données \autoref{classeq:exmpl} ne sont pas équivalentes pour la \textit{test interface} donnée (l'expression \fj{new Static().true()}) premet de les distinguer, car \fj{new Bool()} est différent de \fj{new Other()}.
|
||||
|
||||
Cependant, on pourrait souhaiter que ces classes soient équivalentes, en effet, le nom de la classe est la seule chose qui permet de les différencier car la classe \fj{Bool} de la première class table est en tout point similaire à la classe \fj{Other} de la seconde ! Un programme qui utiliserai la librairie n'aurait jamais à utiliser le nom de la classe du programme et ne saurait distinguer la valeur renvoyée par \fj{Static.true} dans la première class table et dans la seconde.
|
||||
|
||||
@ -986,27 +1019,27 @@
|
||||
\begin{multicols}{2}
|
||||
\begin{fjlisting}
|
||||
\fjclass{Static}{}{
|
||||
\method{Bool}{true}{}{new Bool()}
|
||||
\method{Bool}{false}{}{new Other()}
|
||||
\fjmethod{Bool}{true}{}{new Bool()}
|
||||
\fjmethod{Bool}{false}{}{new Other()}
|
||||
}
|
||||
\fjclass{Bool}{}{
|
||||
\method{Object}{ite}{Object t, Object f}{return t}
|
||||
\fjmethod{Object}{ite}{Object t, Object f}{return t}
|
||||
}
|
||||
\fjclass[Bool]{Other}{}{
|
||||
\method{Object}{ite}{Object t, Object f}{return f}
|
||||
\fjmethod{Object}{ite}{Object t, Object f}{return f}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\columnbreak
|
||||
\begin{fjlisting}
|
||||
\fjclass{Static}{}{
|
||||
\method{Bool}{true}{}{new Other()}
|
||||
\method{Bool}{false}{}{new Bool()}
|
||||
\fjmethod{Bool}{true}{}{new Other()}
|
||||
\fjmethod{Bool}{false}{}{new Bool()}
|
||||
}
|
||||
\fjclass{Bool}{}{
|
||||
\method{Object}{ite}{Object t, Object f}{return f}
|
||||
\fjmethod{Object}{ite}{Object t, Object f}{return f}
|
||||
}
|
||||
\fjclass[Bool]{Other}{}{
|
||||
\method{Object}{ite}{Object t, Object f}{return t}
|
||||
\fjmethod{Object}{ite}{Object t, Object f}{return t}
|
||||
}
|
||||
\end{fjlisting}
|
||||
\end{multicols}
|
||||
@ -1054,7 +1087,7 @@
|
||||
\end{property}
|
||||
|
||||
\begin{property}[Context Lemma]
|
||||
L'objectif de cette nouvelle définition était d'obtenir une sorte de \textit{context lemma}, puisque nous comparrons les expressions sur «toutes les valeurs qu'elles pourraient renvoyer».
|
||||
L'objectif de cette nouvelle définition était d'obtenir une sorte de \textit{context lemma}, puisque nous comparrons les expressions sur \enquote{toutes les valeurs qu'elles pourraient renvoyer}.
|
||||
|
||||
\begin{gather*}
|
||||
\forall CT \forall e_1,e_2\forall (h,CT_c)\\
|
||||
@ -1071,7 +1104,7 @@
|
||||
\left(\forall h \forall \hbar \quad h\left[e_1\right] \rightarrow^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad h\left[e_2\right] \rightarrow^* \hbar\left[\overline{e''}\right]\right)
|
||||
\end{gather*}
|
||||
|
||||
On va déjà montrer le théorème en ajoutant comme contrainte que la réduction $h\left[e_1\right] \rightarrow^* \hbar\left[\overline{e'}\right]$ s'effectue sans application de méthode (\textsc{R-Meth}) à un appel à méthode contenu dans $h$. (C'est à dire que les appels à méthode de $h$ ne «servent à rien», ils pourraient être remplacés par \fj{null} sans modifier la réduction).
|
||||
On va déjà montrer le théorème en ajoutant comme contrainte que la réduction $h\left[e_1\right] \rightarrow^* \hbar\left[\overline{e'}\right]$ s'effectue sans application de méthode (\textsc{R-Meth}) à un appel à méthode contenu dans $h$. (C'est à dire que les appels à méthode de $h$ ne \enquote{servent à rien}, ils pourraient être remplacés par \fj{null} sans modifier la réduction).
|
||||
|
||||
Supposons alors $H_0:\quad \left(\forall \hbar\quad e_1 \rightarrow^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad e_2 \rightarrow^* \hbar\left[\overline{e''}\right]\right)$
|
||||
|
||||
@ -1127,7 +1160,7 @@
|
||||
Nous allons dans cette section essayer de prouver le théorème avec plusieurs class tables en les empêchant d'utiliser des fields non présents dans la test interface.
|
||||
%TODO here
|
||||
\subsection{Petites variations dans la class table}
|
||||
Nous allons dans cette section essayer d'utiliser le lemme des arguments finis dans une seule class table pour essayer de la «modifier» en une class table équivalente en modifiant uniquement le corps d'une seule méthode (ou d'un groupe mutuellement récursif).
|
||||
Nous allons dans cette section essayer d'utiliser le lemme des arguments finis dans une seule class table pour essayer de la \enquote{modifier} en une class table équivalente en modifiant uniquement le corps d'une seule méthode (ou d'un groupe mutuellement récursif).
|
||||
%TODO here
|
||||
|
||||
\newpage
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user