A Trusted Mechanised JavaScript Specification

作者：Bodin Martin^*; Chargueraud Arthur; Filaretti Daniele; Gardner Philippa; Maffeis Sergio; Naudziuniene Daiva; Schmitt Alan; Smith Gareth

来源：ACM Sigplan Notices, 2014, 49(1): 87-100.

DOI：10.1145/2535838.2535876

• JavaScript
• mechanised semantics
• Coq

JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.

• 出版日期2014-1
• 单位INRIA