Publication

Mechanized Semantics for JavaScript Regular Expressions

2024

Résumé

We introduce a mechanization of the JavaScript regexes by transcribing the ECMAScript specification, to which JavaScript conforms, into Coq. We discuss the challenges which arose during this mechanization, and present our efforts to ensure that the result is faithful to the original paper specification. We also use our implementation to prove some properties of the specification, notably that the functions it defines terminate and that no operation ever fails. We extract the implemented engine to OCaml and execute it on test inputs to further increase confidence in its correctness.

Source officielle

https://infoscience.epfl.ch/entities/publication/9b1d1db8-70ad-4735-b6a4-6eccafcaa161

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

2024

Résumé

Source officielle

https://infoscience.epfl.ch/entities/publication/9b1d1db8-70ad-4735-b6a4-6eccafcaa161

À propos de ce résultat

Concepts associés (32)

JavaScript

JavaScript est un langage de programmation de scripts principalement employé dans les pages web interactives et à ce titre est une partie essentielle des applications web. Avec les langages HTML et CSS, JavaScript est au cœur des langages utilisés par les développeurs web. Une grande majorité des sites web l'utilisent, et la majorité des navigateurs web disposent d'un moteur JavaScript pour l'interpréter. JavaScript est aussi employé pour les serveurs Web avec l'utilisation (par exemple) de Node.js ou de Deno.

Expression régulière

vignette|Stephen Cole Kleene, dont les travaux ont fondé le concept d'expression régulière. En informatique, une expression régulière ou expression rationnelle ou expression normale ou motif est une chaîne de caractères qui décrit, selon une syntaxe précise, un ensemble de chaînes de caractères possibles. Les expressions régulières sont également appelées regex (un mot-valise formé depuis l'anglais regular expression). Les expressions rationnelles sont issues des théories mathématiques des langages formels des années 1940.

ECMAScript

ECMAScript est un ensemble de normes concernant les langages de programmation de type script et standardisées par Ecma International dans le cadre de la spécification ECMA-262. Il s'agit donc d'un standard, dont les spécifications sont mises en œuvre dans différents langages de script, comme JavaScript ou ActionScript. C'est un langage de programmation orienté prototype. La société Netscape, à l'origine connue sous le nom de Mosaic Communications Corporation, a développé un langage de script côté client, appelé LiveScript, pour renforcer l'offre commerciale de son serveur web.

Afficher plus

Publications associées (5)

Afficher plus

Mechanized Semantics for JavaScript Regular Expressions

Chattez avec Graph Search

Utility Metrics Specifications. OpenIoT Deliverable D422

Supporting Loop Proofs in KeY by using BLAST

Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications