Towards a Program Logic for 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. The authors 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. They introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with.