- Auteurs : JALLAIS Adrien & SIMON Géraud
- Promotion : IMT FIL 2023 - 3ème année
- Date de rendu : 25/11/2022
Sommaire :
-
- 6.1. Points forts
- 6.1.1. Patron Singleton pour la $CT$
- 6.1.2. TDeclaration et T
- 6.1.3.
Set
représentant les séquences
- 6.2. Points faibles
- 6.1. Points forts
-
- 7.1. Structures de représentation des séquences
- 7.1.1. options 1 : utilisation du type
List
- 7.1.2. option 2 : utilisation du type
Set
- 7.1.3. Conlusion
- 7.1.1. options 1 : utilisation du type
- 7.1. Structures de représentation des séquences
-
- [Fichier de notes](#Fichierdenoteshttps:pad.faire-ecole.orgsQrN2T4Tq_)
- 8.1. Lexique
- 8.1.1. concepts java
- 8.1.2. concepts mathématiques
- 8.1.3. concepts logiques
- 8.1.4. méthodes utilisées
- 8.2. Règles
- 8.2.1. Règles de type
- 8.3. Java vs FJ
Dans le cadre d'une unité d'ensignement d'initiation à la recherche, Rémi Douence a proposé de s'intéresser à une définition rigoureuse des expressions lambdas intégrées par Java 8, avec le papier suivant : Property-based Testing for Lambda-Expressions Semantics in Featherweight Java. (S. da Silva Feitosa,2018). Dans cet article, les auteurs formalisent cette nouvelle fonctionnalité en utilisant des interprètes en Haskell, dont le code est accessible au répertoire suivant : fj-lam.
L'objectif de ce projet est de convertir ces interprètes en Java et de démontrer le bon fonctionnement de nos interprètes en Java.
Pour faciliter la compréhension globale du code, un diagramme de classe a été réalisé :
Le code de ce projet est organisé de la manière suivante :
- Les différentes structures de données de
FJParser.hs
ont été répartis dans le packagesrc.Parser.DefinitionP
, sauf pourExpr
etTypeError
. - Les expressions (
Expr
) ont été regroupées dans le packagesrc.Parser.ExpressionP
et héritent toutes de la classe abstraire java :Expr
. - Les différents types d'erreurs (
TypeError
) ont été regroupées dans le packagesrc.Parser.TypingErrorP
. - Le package
src.Utils
contient la classeFJUtils
, avec les méthodes générales d'évaluation. - Notre traduction de l'approche V1 ne comprend à l'heure actuelle que la traduction de
FJInterpreter.hs
. Celle-ci est disponible dans le packagesrc.V1
- Remarque : Pour
FJInterpreter.java
, les méthodesevalPrime()
etsubst()
sont accompagnées de "sous-méthodes" correspondantes au pattern matching disponible en Haskell selon les types de paramètres (ex:eval' ct (CreateObject c p)
est traduit en Java par la méthodeevalPrime()
qui va appelerevalPrimeAsCreateObject()
).
- Remarque : Pour
Le code de ce projet peut être exécuté en utilisant la fonction main
du fichier ./src/main.java
.
Sous Eclipse, ce projet peut être importé après avoir dezippé le dossier obtenu depuis github, puis après avoir réalisé les actions suivantes : File
> Import
> General
> Import
> Existing Projects into Workspace
> Select root directory
en sélectionnant comme racine le contenu du dossier décompressé > Finish
.
Méthodes | Première implémentation | Testée |
---|---|---|
FJParser |
||
T.TClass |
✅ | ✅ |
T.TInterface |
✅ | ✅ |
Class |
✅ | ✅ |
Interface |
✅ | ❎ |
Method |
✅ | ✅ |
Expr.Var |
✅ | ✅ |
Expr.FieldAccess |
✅ | ✅ |
Expr.MethodInvk |
✅ | ❎ |
Expr.CreateObject |
✅ | ✅ |
Expr.Cast |
✅ | ❎ |
Expr.Closure |
✅ | ❎ |
Type |
✅ | ✅ |
Env |
✅ | ❎ |
CT |
✅ | ✅ |
TypeError.VariableNotFound |
✅ | ❎ |
TypeError.FieldNotFound |
✅ | ❎ |
TypeError.ClassNotFound |
✅ | ❎ |
TypeError.MethodNotFound |
✅ | ❎ |
TypeError.ParamsTypeMismatch |
✅ | ❎ |
TypeError.WrongClosure |
✅ | ❎ |
TypeError.WrongCast |
✅ | ❎ |
TypeError.UnknownError |
✅ | ❎ |
FJUtils |
||
subtyping |
✅ | ❎ |
fields |
✅ | ❎ |
methods |
✅ | ❎ |
mbody |
✅ | ❎ |
isValue |
✅ | ❎ |
FJInterpreter |
||
eval' |
✅ | ❎ |
eval |
✅ | ❎ |
subst |
✅ | ❎ |
Les tests qui ont pu être réalisés se résument à s'assurer que les objets créés par l'instanciation de la classe C
(correspondant au type definition). Ces instanciations ont permis des tester l'ensemble des classes du package src.Parser.DefintionP
.
FJUtils |
||
absmethods |
mtype |
lambdaMark |
removeRuntimeAnnotation |
||
FJTypeChecker |
||
throwError |
typeof |
methodTyping |
classTyping |
interfaceTyping |
ctTyping |
FJGenerator |
||
maybeElements |
pickVar |
genClassName |
genInstantiableType |
genClassType |
genInterfaceTypeList |
genVar |
genAttrs |
genMethod |
genSign |
genMethods |
genClass |
genInterface |
addClass |
addInterface |
addType |
genClassTable |
genCreateObject |
genFieldAccess |
genMethodInvk |
genCast |
genClosure |
ccreateobject |
cfieldaccess |
cmethodinvk |
cucast |
cdcast |
cscast |
cclosure |
genExpr |
genExpression |
instance Arbitrary |
Il n'est possible d'instancier qu'une seule fois la classe CT
(class table
Les types correspondants à des Interfaces (src.Parser.DefinitionP.I
) ou des Classes (src.Parser.DefinitionP.C
) étendent tous les deux le type extends
commun aux interfaces et aux classes.
Il est prévu également une autre factorisation de code pour la déclaration du corps des classes et des interfaces qui comportent toutes deux des méthodes.
Pour réprésenter des séquences (ex. TreeSet
pour se protéger des duplications des données, tout en gardant une structure de données itérable.
Cela est particulièrement utile pour les séquences d'interfaces (
Seule l'approche V1 a pu être explorée et traduite dans notre projet, faute de temps.
Par ailleurs, nous n'avons pas pu traduire l'ensemble des méthodes de la V1 vers le Java.
De plus, certaines des méthodes qui ont pu être implémentées n'ont pas pu être toutes testées et optimisées (i.e temps d'exécution et de ressources consommées (nombre d'appels entre les objets, redondances des boucles...)).
Comme le montre les points suivants, plusieurs choix on pu être réalisés lors de l'implémentation des interpréteurs.
- Emballer variables de type String dans des classes (ex.
TypeName
dans la classeType
). - Utilisation de structures de représentation des séquences (ex.
Set
à la place deList
ouArray
).
Dans la partie suivante nous discuterons de ce dernier choix.
Dans l'article les auteurs utilisent des séquences (List
ou du type Set
.
- limite la possibilité d'un
ArrayOutOfBound
- facilite le parcours des données
- maintient l'ordre d'insertion
- pas de comparaisons entre les données
- pas de protection contre les doublons (il aurait pu être possible de le faire manuellement en redéfinissant des
equals()
à chaque type d'Expr
, mais cela aurait été fastidieux et source d'erreurs potentielles)
- protection contre les doublons
- le type
Set
n'autorise qu'une seule valeur nulle dans la collection. Comme le code (cf.FJUtils
etFJInterpreter
) contient déjà des contrôles pour éviter qu'un null soit inséré dans une collection, cette caractéristique de structure donnée était adéquate à notre utilisation
- moins adapté pour les parcours que le type
List
- nécessite un temps de travail supplémentaire pour la définition de l'implémentation de l'interface
Comparable
Notre première version du projet utilisait des tableaux pour les structures de données (ex. en attribut de la classe Signature.java
, on avait Field[] params
).
Ce choix avait été pris pour les cas où nous étions sûrs que les données étaient définies, et donc que la taille du tableau serait fixe.
La seconde version du projet utilisait des listes (List
puis ArrayList
).
L'objectif principal était de limiter la possiblité d'un ArrayOutOfBound
(dépassement de la taille du tableau quand on le parcourt ou quand on y ajoute un nouvel élément). Ensuite, les listes permettaient une navigation plus simple dans les parcours, comme dans les boucles for
, avec plus de flexibilité que les tableaux.
Une première implémentation était l'utilisation du type List<>
dans les signatures des méthodes, puis dans l'implémentation un ArrayList<>
. Cela offre un code plus sûr et plus adapté aux pratiques professionnelles. Cependant, pour simplifier temporairement le code, nous sommes passés à utiliser ArrayList<>
à chaque occurence.
Nous avions le choix entre ArrayList
et LinkedList
:
ArrayList
reproduit une structure sous forme de tableau (basée sur l'index d'un élément) et permet de faciliter les get(), ce qui nous semblait le plus pertinent à cette phase du projet.LinkedList
lie les objets de la liste entre eux, ce qui fait que pour récupérer un élément précis, il faut parcourir chaque élément de la liste pour le trouver. Nous avons conclu que l'ArrayList
était plus pertinent pour optimiser les accès aux éléments de la liste.
La troisième et actuelle version utilise des sets (TreeSet
).
L'objectif était de protéger nos séquences en évitant d'y insérer des doublons.
- Nous avons fait le choix du format
TreeSet
pour garder en mémoire l'ordre d'insertion des objets, et pouvoir utiliser des index sur la structure de données. Ce cas à notamment était nécessaire lors de l'implémentation de la méthodeeval'
dans le cas desFieldAcess
, où on utiliseData.List.findIndex
pour récupérer l'index d'un élément, puis retourner l'élément lié à cet index.
Dans le cas où nous devrions refaire ce projet d'initiation à la recherche, nous aurions demandé quelle était la priorité entre finir la compréhension de l'article ou bien l'implémentation des interprètes en Java.
Dans notre cas, nous avons accordé beaucoup de temps lors de nos premières séances à la lecture de l'article, ce qui nous a empêché de nous intéresser au code en Haskell et de commencer à coder, ce qui pourrait expliquer une v1 non terminé.
Si nous avions à recommencer, nous aurions une courbe d'apprentissage sur la compréhension d'Haskell moins longue.
-
functional interface
: interface possédant une et une seule méthode abstraite (dont seule la signature est indiquée) -
abstract method
: une méthode sans implémentation -
default method
: une méthode déclarée dans une interface, et qui possède une implémentation par défault -
$\lambda$ -expression
/$\lambda$ -fonction
: fonction anonyme qui implémente une interface fonctionnelle mais qui est écrit sans type.- Elles ne peuvent cependant être appelées sans type
- Elles permettent au programme de traiter les fonctions comme l'argument de méthode
-
Object
: Base class of every class, which has no fields (so the invocations of super have no arguments) and no methods -
target type
: type d'une$\lambda$ -expression
inféré par le compilateur en fonction du contexte de celle-ci. Ce type est nécessaire pour que la$\lambda$ -expression
puisse être invoquée -
type elaboration
: la tâche de construire une représentation explicitement typée du programme -
type inference
: le problème de déterminer si un programme est bien typé -
type soudness
: le système de types de Java est sain (sound), dans le sens où, à moins qu'une exception ne soit levée, l'évaluation de toute expression produira une valeur d'un type "compatible" avec le type qui lui est attribué par le système de types (cf. ref) -
type judgement
: jugement du type d'une expression (représenté par$\leadsto$ )- quand le
type judgement
est appliqué sur une expression$e$ , il produit un couple :$\langle T , e'\rangle$ , avec$T$ le type de cast et$e'$ une nouvelle expression
- quand le
-
cast
:$\Gamma \vdash e : \langle T, e' \rangle$ <=> soit une expression$e$ composée d'une expression$e'$ annotée par le type$T$ / castée en$T$ -
params
vs.args
: on définit les paramètres d'une fonction, qu'on appelle en lui passant des arguments
-
$x : T$ : on associe à la variable$x$ un type$T$ -
$\overline{x}$ : séquence possiblement vide de$x$ -
$\bullet$ : séquence vide <=>[]
-
$\sharp \overline{x}$ : taille de la séquence de$x$ -
$\langle \rangle$ : couple dont l'ordre est à prendre en compte (à la différence d'une paire) -
$( \overline{T} \overline{x} )$ : séquence de paramètre$x$ qui sont de type$T$ -
$T <: U$ ou$T <: \overline{U}$ :$T$ est sous type de$U$ ou de toutes les occurences de$\overline{U}$ respectivement -
$( \overline{T} \overline{x} ) \rightarrow e$ : définition formelle d'une fonction anonyme (d'une$\lambda$ -expression
) de$\sharp x$ paramètres, dont le corps est défini par l'expression$e$ -
$\Gamma$ : représente un mapping fini :$\overline{x}:\overline{T}$ , reliant les variables$x$ (leur nom) à leur type$T$ => définir le contexte/environnement-
$\Gamma \vdash E : T$ : "Dans le context$\Gamma$ , l'expression$E$ est de type$T$ "
-
-
$CT$ : représente une table qui associe le noms des interfaces ou des classes à leur déclaration ($L$ ou$P$ ) => mémoriser le programme source
- séquent : conjonction d'hypothèses
$\vdash$ disjonction de conclusion - règles :
$\frac{premises}{conclusion}$ de séquent
qui dit que nous pouvons conclure que
-
mtype
: permet d'obtenir le type d'une méthode m dans une classe C, en renvoyant une paire de[liste de Type, Type]
<=>types de paramètres de la méthode et le type de rentour de la méthode
-
mbody
: permet d'obtenir une paire de(liste de String, Expr)
<=>liste des paramètres, expression
-
$\lambda$ mark
: fonction qui ajoute, lors du run-time, une définition decast
si et seulement si la$\lambda$ -expression
apparaît dans le code source -
fields
: fonction qui renvoie une liste(Type, String)
<=>liste composée du tpye et du nom de chaque attributs
Si dans notre environnement, on a une variable
Alors son type peut être jugé tel que
Autrement dit, son type la variable
Si dans notre environnement, il existe une expression
Alors le type d'un attribut
Autrement dit, si l'on peut caster une classe
Si l'on définit une méthode mtype
prenant en paramètre le nom d'une méthode (mark
, en produisant une nouvelle liste
Alors, la méthode mark
).
Après que les attributs (de type mark
,
si l'on note que ces nouveaux attributs annotés peuvent être castés en un autre sous type (
Alors, un constructeur peut être appelé avec des paramètres castés si ces paramètres sont d'un type qui étend le type des paramètres d'origine.
Si l'on a pu caster une expression
Alors cette expression implémente une interface fonctionnelle.
Si une expression implémente une interface fonctionnelle,
et que l'on peut y appliquer mark
sur le corps de sa méthode, produisant ainsi une nouvelle expression
Alors, l'expression
Produit une nouvelle instance de méthode, contenant le corps d'une expression possiblement annotée.
Vérifie qu'une classe est bien formée.
Vérifie qu'une interface est bien formée, en regardant en plus de Class typing, que l'interface n'a ni constructeur ni attribut, et qu'elle contient au moins une méthode abstraite.
Featherweight Java (FJ) est une version allégée de Java, mais dont la sémantique est rigoureusement définie. Elle a été introduit par l'article suivant : Featherweight Java: A minimal core calculus for Java and GJ (Igarashi et al., 2001).
Java | Haskell |
---|---|
FJ |
-calculus
|
Les fonctionalités Java suivantes sont absentes de FJ :
- impact des opérations d'objets sur les attributs en mémoire,
- interfaces,
- surcharges
- appels au méthode des classes de base,
- pointeur null
- types de basases
- méthodes abstraite
- états
- control d'accès
- exceptions
Java | FJ |
---|---|
structural types | nominal types |
gantt
dateFormat DD-MM-YYYY
axisFormat %m-%d
title [IMT-FILA3-CapiTrain] Log
section seances planifiées
seance1 : w1, 14-10-2022, 1d
seance2 : w1, 28-10-2022, 1d
seance3 : w1, 04-11-2022, 1d
seance4 : w1, 16-11-2022, 1d
seance5 : w1, 18-11-2022, 1d
seance6 : w1, 20-11-2022, 1d
seance7 : w1, 24-11-2022, 1d
seance8 : w1, 25-11-2022, 1d
section avancement en autonomie
autonomie1 : a1, 07-11-2022, 1d
autonomie2 : a1, 10-11-2022, 1d
autonomie3 : a1, 14-11-2022, 1d
autonomie4 : a1, 15-11-2022, 1d
autonomie5 : a1, 19-11-2022, 1d
autonomie6 : a1, 20-11-2022, 1d
autonomie7 : a1, 23-11-2022, 1d
section dates importantes
présentation : milestone, 07-10-2022, 1d
rendu : milestone, 25-11-2022, 1d
soutenance : milestone, 28-11-2022, 1d
Afin de faciliter l'implémentation de nos interpréteurs en Java, une lecture attentive du code en Haskell écrit par les auteurs (fj-lam) a été réalisée. Une version commentée de ce code est disponible dans le dossier suivant : ./fj-lam.