A formal specification of the semantics of ECMAScript

Web applications (i.e., applications whose interface is presented to the user via a web browser, whose state is split between a server and a client, and where the only interaction between server and client is through the HTTP protocol) are become more and more widespread, and integrated in most users' everyday work habits. The glue linking the desperate technologies involved, from dynamic HTML to XML RPC, is the Javascript language. Yet, no formal definition of its semantics exists, which in turn makes it impossible to formally prove correctness, liveness and security properties of Web applications. As a first step towards improving this situation, we provide a formal semantics for ECMAScript (standard ECMA-262), by means of an Abstract State Machines (ASMs) specification. We follow the path established by other specification efforts for similar languages (e.g. Java and C#), but in addition we establish a formal trace between parts of our specification and the ECMA standard, thus facilitating the proof of correctness of the specification. More specifically, we define the dynamic semantics of ECMAScript by providing (in terms of ASMs) an interpreter which executes ECMAScript programs. We use an algebra to represent the state of the ECMAScript program, the state of the ECMAScript interpreter, and the state of the host environment (typically, the browser). We assume the necessary syntactic information (namely, the annotated Abstract Syntax Tree (AST) of the given program) to be available. Using ASM we detail a visit of the AST, whose effect is to simulate the execution of the program. In the ECMA standard the behavior of ECMAScript constructs is operationally described using so-called abstract operations (AO), coming as numbered lists of steps. Therefore our interpreter is composed out of two submachines: ECMA-Script and ECMA-AO interpreters. The former invokes the ECMA-AO one to evaluate nodes, simulating AOs used in ECMA standard to describe the production's semantics. We organize the ECMA-AO interpreter rules in such a way that each rule application corresponds to an AO instruction in the ECMA standard. This helps to check the correctness of the ASM model wrt the ECMA standard as well as the correctness of implementations wrt ASM model. Therefore, the state of our interpreter can be mapped via abstraction/refinement functions onto the concrete state of any comformant implementation.