Towards a Program Logic for JavaScript
Towards a Program Logic for JavaScript
复制标题
DOI：
10.1145/2103621.2103663
复制
发表时间：
2012-01-01
影响因子：
--
通讯作者：
Smith, Gareth
中科院分区：
文献类型：
--
作者：
Gardner, Philippa;Maffeis, Sergio;Smith, Gareth
JavaScript已成为客户端Web编程中使用最广泛的语言。JavaScript的动态特性使得理解它的代码非常困难，导致程序错误和缺乏足够的静态分析工具。我们相信，逻辑推理有很多提供JavaScript：一个简单的程序行为的描述，模块边界的清晰理解，并能够验证安全contractions.We介绍了一个程序逻辑推理的广泛子集的JavaScript，包括具有挑战性的功能，如原型继承和。我们采用分离逻辑的思想来提供关于JavaScript代码的易处理的推理：关于简单程序的推理是容易的;关于困难程序的推理是可能的。我们证明了一个强可靠性的结果。在我们的子集中编写的所有库，并证明其规范是正确的，即使被任意JavaScript代码调用，也将表现良好。
JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts.We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with. We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.