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....

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Philippa Gardner, Sergio Maffeis, Gareth David Smith
• Keywords: Logic Web, Module Boundaries, POPL 2012, Programming Languages, Reliability Theory