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.
This work will be published in POPL 2012.
Invited talk at FOOL 2011; Sunday, 23 October 2011; Portland, Oregon, USA