# Spécification de JavaScript

La spécification d'un langage est une définition de la syntaxe et de la sémantique du langage. Cette définition est en général un ensemble de règles syntaxiques définies dans une grammaire.
Initialement dédiés au partage de contenus statiques sur Internet, les sites web sont devenus de véritables applications accessibles à partir de n'importe quel navigateur.
Afin de rendre les sites plus interactifs et dynamiques, il a été nécessaire de mettre en place des langages de script tel que l'ActionScript ou le JavaScript. Ce dernier est actuellement le langage le plus utilisé pour les applications côté client, c'est-à-dire sur le navigateur.
L'ECMAScript a vu le jour en 1997 dans le but d'uniformiser l'interprétation de ces différents langages de script. Cette spécification décrit la syntaxe et la sémantique que ces langages doivent respecter, sous forme de phrases littérales. Ces définitions étant sujettes a interprétation, on a vu apparaître des divergences d'un langage, ou d'une de ses implémentations, à l'autre. La formalisation de cette spécification EcmaScript permettrait de lisser ces différences d'interprétation.

## Motivations

La norme ECMAscript ne décrit pas le comportement à adopter par JavaScript de façon précise du fait que les règles sont définies avec des phrases littérales. En effet, chaque description de la spécification peut être comprise et interprétée différemment, ce qui a mené à l'apparition de divers interpréteurs JavaScript, ou même encore de primitives spécifiques aux moteurs de certains navigateurs, notamment entre Internet Explorer et Mozilla Firefox. Cette différence d'interprétation entre Internet Explorer et les autres navigateurs provient du fait que lors de la création du JavaScript par Brendan Eich en 1995, Microsoft a développé sa propre version avant que la norme EcmaScript apparaisse. Ceci est la raison pour laquelle un script fonctionnant correctement sous Internet Explorer ne fonctionnera pas forcément sur un autre navigateur. Dans le but d'assurer une compatibilité optimale entre les différents navigateurs, il est nécessaire de définir une spécification formelle afin que tous les interpréteurs acceptent la même syntaxe.
De plus, le JavaScript possède des vulnérabilités, quant au bon déroulement d'un programme, dues à certains cas non décrits dans la norme ECMAScript. Prenons par exemple le cas de l'opérateur typeof : la norme ne décrit pas explicitement quel comportement adopter si l'évaluation de l'expression unitaire provoque une erreur, laissant la possibilité ici d'un comportement variable selon les implémentations. Il est ainsi nécessaire aux analyseurs de gérer ce genre de problèmes. Les différentes interprétations n'assurent donc pas un comportement uniforme des programmes JavaScript, c'est pourquoi plusieurs recherches se portent sur la formalisation de ce langage.

## Approches

On relève dans la communauté scientifique au moins 3 approches sur cette question.

### λJS : l'essence de JavaScript

Cette approche part de deux constats : d'une part, le JavaScript n'est pas sécurisé à cause d'une sémantique non conventionnelle ; d'autre part, le langage est trop complexe pour être testé par des outils de tests standard. C'est sur ces deux points que se sont portés les travaux de Arjun Guha, Claudiu Saftoiu et Shriram Krishnamurthi.
Leur premier travail a été de concevoir un noyau, nommé λJS, qui ne contient que les fonctions essentielles du langage, sorte de sous-ensemble complet de JavaScript. Bien sûr, le fait de ne garder que l'essence du langage fait que beaucoup de sucre syntaxique n'existe plus. Prenons, par exemple, l'implémentation des objets, où certaines syntaxes ont été supprimées, au privilège d'une seule lorsque plusieurs sont envisageables. Afin d'accéder à l'attribut x d'un objet Y, il est normalement possible d'écrire Y['x'] ou Y.x. Cependant, λJS ne possède que l'écriture Y['x'] et n'implémente pas d'écriture alternative afin de garder le noyau de langage le plus petit possible. Une autre modification majeure est la disparation de l'utilisation implicite du this. En effet, lorsque l'on utilise le mot clé this, le programme fait référence à l'objet sur lequel est appelée la fonction. Toutefois, ce paramètre est implicite, il n'est donc pas nécessaire de le renseigner lors de l'appel de la méthode d'un objet, ce qui n'est pas le cas avec λJS. Ils ont ainsi fait disparaître un grand nombre de sucres syntaxiques dans le but de minimiser l'implémentation des fonctions pour permettre plus facilement la vérification d'un programme.
Cependant, afin de faire accepter leur noyau par les autres développeurs, il est nécessaire pour eux de prouver que n'importe quel programme écrit en JavaScript peut être réduit en un programme basé sur λJS. Pour réaliser leurs tests, l'équipe s'est basée sur trois implémentations de Javascript : SpiderMonkey (Firefox), V8 (Chrome), et Rhino (implémentation en Java). Ils ont transformé différents programmes compatibles sur ces implémentations vers un programme λJS, et ont ensuite vérifié que la sortie du nouveau programme correspond à celle de la version d'origine. Afin de couvrir un maximum de cas, les programmes sont un échantillon important de la série de test JavaScript de Mozilla. Les tests ont été concluants : l'intégralité de la série de tests produit exactement le même résultat que les trois autres implémentations.
L'objectif final étant de fournir un langage sûr, il est nécessaire de fournir un outil permettant de vérifier ce résultat. Le λJS étant une implémentation simplifiée du JavaScript, et étant donné qu'un programme peut être réduit en λJS, il est nécessaire de montrer que λJS est sûr. Pour prouver ceci, ils ont décomposé chaque propriété en sous-problèmes. Pour illustrer, prenons le cas de l'addition : ils jugent qu'une addition e1 + e2 est sûre si les expressions e1 et e2 sont sûres. En posant plusieurs lemmes, ils démontrent que l'addition est sûre et qu'elle peut être incluse dans le λJS. En appliquant cette démarche sur plusieurs éléments du langage, ils ont réussi à inclure un grand nombre de fonctionnalités à leur noyau en le gardant sûr. Ceci a permis en 2012 de définir le λJS comme base pour le langage JavaScript par ECMAScript 6, toutefois cette version n'est pas encore totalement supportée par tous les navigateurs.

### SAFE : une autre specification pour EcmaScript

SAFE (Scalable Framework Analysis for ECMAScript) est un projet mené par le groupe de recherche en langage de programmation de l'Institut supérieur coréen des sciences et technologies (KAIST).
Tout comme le papier précédent, l'équipe se penche ici sur le constat que la spécification informelle du langage rend celui-ci sujet à interprétation. L'équipe relève également que les différents moteurs Javascript ne sont pas assez documentés, rendant leur compréhension et leur modification difficile. Ceci était le cas avec λJS qu'ils ont souhaité utiliser : ils ont jugé que la documentation concernant la réduction du Javascript en leur noyau n'était pas assez détaillée. C'est en partant de ces deux propositions qu'ils ont débuté le projet SAFE qui a pour but d'améliorer l'analyse d'un programme Javascript ainsi que de fournir un outil documenté pour la recherche.
SAFE est développé à destination de la communauté de recherche en JavaScript, c'est un projet open-source dont le code est accessible en ligne. L'implémentation est réalisée en Java et en Scala.
Comparé à l'approche de λJS, l'équipe ne s'est pas contentée de réduire un maximum de langage afin de fournir une spécification simplifiée mais a préféré réaliser une spécification de l'ensemble du langage. C'est dans ce sens qu'ils ont défini une spécification sur chaque niveau de représentation d'un programme Javascript.

#### L'arbre de syntaxe abstrait : AST

Afin de réaliser leur framework, il a été dans un premier temps nécessaire de transformer le code Javascript en un code facilement analysable.
Pour ce faire, le framework se base sur 3 niveaux de représentation d'un programme Javascript. La première représentation (qui est la plus proche du code source) est un AST (Arbre syntaxique abstrait). Afin d'obtenir l'AST correspondant au code source analysé, l'équipe s'est intéressée aux parsers JavaScript existants (ANTLR, les combinateurs de parseur de Scala, Rhino, SpiderMonkey, Closure Tools de Google, JSConTest, ou encore JSure) sans trouver entière satisfaction. Elle a finalement utilisé l'outil de génération Rats! se trouvant dans le projet eXTensible Compiler développé par une équipe de New York. Elle fournit à Rats! une grammaire de style BNF dont voici l'extrait concernant les instructions de boucle (l'indentation représente une relation de sous-classe) :
Rats! génère alors un parser JavaScript en langage Java, qui couplé à ASTGen, qui génère les classes Java représentant l'AST à partir d'une description fournie, va permettre de transformer le code JavaScript en représentation intermédiaire.

#### La représentation intermédiaire : IR

Dans un second temps, le framework transforme l'AST en une représentation intermédiaire IR qui permet de fournir une spécification de chaque fonctionnalité du langage Javascript définie par ECMAScript. Par exemple, chaque fonction possède au moins l'argument this afin de respecter cette norme. C'est cette représentation qui est utilisée pour l'évaluation du programme par un interpréteur. C'est à ce niveau qu'intervient SAFE en fournissant une spécification formelle et une implémentation de chaque fonctionnalité.
Grammaire de JavaScript IR :

#### Le graphe de flot de contrôle : CFG

Le troisième niveau de représentation est le CFG (Graphe de flot de contrôle) qui est utilisé uniquement pour l'analyse des performances. Afin de générer ce graphe, le projet utilise CFGBuilder qui est un composant du compilateur Polyglot. Ce programme prend en paramètre une représentation intermédiaire et génère un graphe correspondant qui pourra ensuite être analysé par le framework afin de réaliser plusieurs analyses.
Un exemple de transformation du code JavaScript au graphe de contrôle de flot en passant par la représentation intermédiaire, proposé dans le paragraphe 3.3 dans la publication présentant SAFE, illustre bien le résultat obtenu à ce stade.

#### Applications

Leur framework est disponible au public. Afin de permettre l'utilisation de leur projet par le plus grand nombre, SAFE fournit, en plus de la spécification et d'une documentation fournie, une implémentation des différentes fonctionnalités. Ceci permet d'utiliser leurs recherches plus facilement que les autres projets qui n'ont pas ou peu de documentation.
Les 3 niveaux de représentation du code JavaScript (AST, IR, CFG) rendent SAFE plus flexible, évolutif, et connectable, proposant ainsi un outil puissant dans la recherche et le développement de JavaScript.

### JSCert : une spécification mécanisée et sûre de JavaScript

"Le projet JSCert a pour but de vraiment comprendre JavaScript", annonce le site du projet. Une équipe de chercheurs des laboratoires de l'INRIA et de l'Imperial College London se sont intéressés à la nécessité de clarifier les ambiguïtés liées à la longueur et aux nombreux recoins du standard ECMAScript.

#### JSCert

JSCert est une spécification mécanisée du standard ECMAScript, écrite dans l'assistant interactif de preuve Rocq, conçue pour être la plus proche de la norme ECMAScript5. Elle se base sur le développement en 2008, mené par Sergio Maffeis, d'une sémantique de description formelle du comportement complet de JavaScript suivant fidèlement ECMAScript3, à l'exception des parties ambiguës de ce standard. Cette formalisation se limite au cœur du langage JavaScript.

#### JSRef

En parallèle a été développé JSRef, un interpréteur exécutable de référence, certifié dans le respect de JSCert, et testé en utilisant la suite de tests de confirmité d'ECMAScript, test262.
JSCert n'est pas directement utilisable, de par sa conception : c'est une définition inductive à destination du développement de preuves de sûreté, qui compense l'imprécision concernant les fonctionnalités dépendantes de l'implémentation dans ECMAScript5. En tant que spécification Rocq calculable, on en a extrait automatiquement le code OCaml correspondant, obtenant ainsi l'interpréteur JSRef. Celui-ci respecte la norme ECMAScript5 autant qu'il était possible de la formaliser par JSCert.

#### De ECMAScript à JSRef

La vérification de JSCert dans cette sémantique mécanisée est dû à sa proximité avec la norme ECMAScript5 : la prose anglaise de celle-ci et les règles formelles qui en découlent peuvent être mises côte-à-côte, chaque ligne de pseudo-code correspondant à une ou deux règles formelles de JSCert. JSRef se vérifie par le mécanisme automatique par lequel il est extrait de JSCert.
Le pseudo-code correspondant à la boucle while dans ECMAScript5 :
La sémantique JSCert implémentée dans Rocq correspondant à la boucle while, et traduisant la sémantique définie dans la publication de JSCert :
La sémantique JSRef de la boucle while :

#### Applications

On peut envisager plusieurs utilisations potentielles de JSCert et JSRef :
* analyser des morceaux de code JavaScript
* vérifier la bonne implémentation d'un compilateur d'un langage de plus haut niveau en JavaScript
* comparer l'implémentation d'un interpréteur avec celle de JSRef
On peut imaginer que cette spécification formelle et mécanisée soit intégrée dans une future édition d'ECMAScript.

## Synthèse

| | λJS | SAFE | JSCert |
| Motivation | Pouvoir tester plus efficacement des programmes Diminuer la complexité des programmes | Améliorer l'analyse des programmes Fournir des outils pour la recherche | Fournir une représentation formelle de l'ECMASCRIPT Clarifier ECMAScript en cas de doute sur l'interprétation Fournir un interpréteur vérifiant qu'un programme respecte cette spécification |
| Réalisations | Réalisation d'un noyau minimal de Javascript Assurer la sureté de ce noyau Ramener le sucre syntaxique aux fonctions de base | Fournir une spécification et une implémentation de l'ECMAScript Convertir l'AST d'un programme Javascript vers une représentation intermédiaire | Réalisation d'une spécification formelle des fonctionnalités de Javascript Réalisation d'un interpréteur respectant JSCert |
| Spécification effectuée | Réduction du Javascript en un ensemble de fonction minimale | Spécification sur chaque niveau de représentation d'un programme Javascript | Réalisation d'une spécification en Rocq |