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.