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.