Towards a program logic for JavaScript
Towards a program logic for JavaScript
复制标题
DOI：
10.1145/2103656.2103663
复制
发表时间：
2012-01
期刊：
影响因子：
--
通讯作者：
Philippa Gardner;S. Maffeis;Gareth Smith
中科院分区：
文献类型：
--
作者：
Philippa Gardner;S. Maffeis;Gareth Smith
JavaScript已成为客户端Web编程的最广泛使用的语言。 JavaScript的动态性质使得众所周知其代码很难理解，导致了越野车计划和缺乏足够的静态分析工具。我们认为，逻辑推理可以提供JavaScript：简单地描述程序行为，对模块边界的清晰了解以及验证安全合同的能力。我们介绍了一个程序逻辑，以推理有关JavaScript的广泛子集，包括具有挑战性的功能，例如原型继承和“ With”。我们调整了分离逻辑中的想法，以提供有关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.