A trusted mechanised JavaScript specification
A trusted mechanised JavaScript specification
复制标题
值得信赖的机械化 JavaScript 规范
DOI：
10.1145/2535838.2535876
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Bodin M
中科院分区：
文献类型：
--
作者：
Bodin M
JavaScript是客户端应用程序中使用最广泛的Web语言。虽然JavaScript的开发最初只是由实现主导的，但现在ECMA标准化进程背后的动力越来越大。一个正式的、机械化的JavaScript规范的时机已经成熟，它可以澄清ECMA标准中的歧义，为高级语言编译和JavaScript实现提供可信的参考，并为语言属性的高保证证明提供一个平台。从Coq到OCaml提取的JavaScript的参考解释器。我们给出了一个Coq证明，JSRef是正确的JSCert和评估JSRef使用test262，ECMA一致性测试套件。我们的方法确保了JSCert是一个相对准确的英语标准的制定，这只会随着时间的推移而改进。我们已经证明，现代技术的机械化规范可以处理JavaScript的复杂性。
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.
登录
查看更多内容
状态报告：使用 ML 指定 javascript
DOI：
--
发表时间：
2007
期刊：
ML Workshop
影响因子：
--
作者：
David Herman;C. Flanagan
通讯作者：
C. Flanagan
JavaScript 的操作语义
DOI：
--
发表时间：
2008
期刊：
Asian Symposium on Programming Languages and Systems
影响因子：
--
作者：
S. Maffeis;John C. Mitchell;Ankur Taly
通讯作者：
Ankur Taly
DOI：
--
发表时间：
2011-08
期刊：
ArXiv
影响因子：
--
作者：
J. Politz;Spiridon Aristides Eliopoulos;Arjun Guha;S. Krishnamurthi
通讯作者：
J. Politz;Spiridon Aristides Eliopoulos;Arjun Guha;S. Krishnamurthi
影响因子：
1.1
作者：
E. Börger;Nicu G. Fruja;V. Gervasi;R. Stärk
通讯作者：
R. Stärk
DOI：
10.1007/978-3-540-31987-0_28
发表时间：
2005-04
期刊：
--
影响因子：
--
作者：
Peter Thiemann
通讯作者：
Peter Thiemann