Towards a program logic for JavaScript

7 years 9 months ago
Towards a program logic for JavaScript
JavaScript has become the most widely used language for clientside 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. Categories and Subject Descriptors F.3....
Philippa Gardner, Sergio Maffeis, Gareth David Smi
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where POPL
Authors Philippa Gardner, Sergio Maffeis, Gareth David Smith
Comments (0)