JavaScript is the most actively used programming language on GitHub, and there are diverse language implementations, including engines, analyzers, compilers, etc. JavaScript is designed with a language specification called ECMA-262, maintained by TC39, and the language implementations are developed based on it. While the specification is written in highly structured prose, there has been no automated mechanism to check its correctness and conformance. In addition, since 2015, TC39 has decided to release ECMA-262 annually to ensure the rapid adoption of new language features, making it more challenging to maintain correctness and conformance. To address these problems, we introduced a novel approach to extract a mechanized specification from a prose specification automatically and showed how useful it can be in practice. First, our tool automatically extracts a mechanized specification from a prose specification. It generates a JavaScript parser from language syntax and compiles abstract algorithms into metalanguage functions to represent the language semantics. There are diverse ways to utilize the extracted mechanized specification: 1) conformance test synthesis to check discrepancies between language implementations and the specification, 2) type analysis on the language specification to detect specification type errors, and 3) generation of special-purpose language implementations, such as JavaScript static analyzers, in a correct-by-construction manner. We have open-sourced all these tools as “ESMeta” and made them practically available in the JavaScript language development process.

Jihyeok Park is an Assistant Professor at the Dept. of Computer Science and Engineering, College of Informatics, Korea University. My main research topic is programming languages and software engineering, including program analysis, mechanized specification, program synthesis, and automated testing. I’m also leading an open-source project, ESMeta, which is a framework that extracts a mechanized specification from a given version of ECMAScript specification (ECMA-262) and automatically generates language-based tools.