Local reasoning about Web programs

• Main Author: Smith, Gareth David
• Other Authors: Gardner, Philippa ; Drossopoulou, Sophia
• Published: Imperial College London 2011
• Subjects: 005.3
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.537244

Since 1990, the world wide web has evolved from a static collection of reference pages to a dynamic programming and application-hosting environment. At the core of this evolution is the programming language JavaScript and the XML update library "DOM". Every modern web browser contains a DOM implementation which allows JavaScript programs to read and alter the web page that the user is currently viewing. JavaScript and DOM are extremely successful, and this success may be in part due to their highly dynamic and tightly integrated nature. However, this very nature hinders formal program analysis and tool development. Even the implementation independent specification that defines DOM is largely written in the English language, and not using any formal system. While client-side web programming was once a simple discipline of form validation and interface trickery, it is fast becoming a far more serious business encompassing application development for the emerging ubiquitous "cloud". As this evolution gains pace there is an increasing demand for client-side tool support of the sort commonly enjoyed by "enterprise" programmers, working in more easily analysed languages such as Java. This thesis makes use of recent developments in program reasoning using context logic to provide the first formal, compositional specification for the Fundamental Interfaces of DOM Core Level 1. It presents both a big-step operational semantics for the necessary operations of the library and a context logic for reasoning about programs which use the library. Finally, it presents example programs that use the library and shows how context logic can be used to prove useful properties of those programs.