A Trusted Mechanised JavaScript Specification

Gareth Smith, Imperial College.

A Trusted Mechanised JavaScript Specification

JSCert Logo http://jscert.org/popl14/

A Trusted Mechanised JavaScript Specification

JavaScript Specifications

This Talk

JSCert Trust

Coverage

JSCert Coverage

Coverage

JSCert Coverage

ES5 ↔ JSCert

Connecting ES5 to JSCert

ES5 ↔ JSCert

Connecting ES5 to JSCert

ES5 ↔ JSCert

Connecting ES5 to JSCert

Reading the Coq

This:
red_stat_while1
Can be read as this:
red_while_2a_2b

While

  1. Let V = empty.
  2. Repeat
    1. Let exprRef be the result of evaluating Expression.
    2. If ToBoolean(GetValue(exprRef)) is false, return (normal, V, empty).
    3. Let stmt be the result of evaluating Statement.
    4. If stmt.value is not empty, let V = stmt.value.
    5. If stmt.type is not continue || stmt.target is not in the current label set, then
      1. If stmt.type is break and stmt.target is in the current label set, then
        1. Return (normal, V, empty).
      2. If stmt is an abrupt completion, return stmt.

While

  1. Let V = empty.
red_while_1

While

  1. Repeat
    1. Let exprRef be the result of evaluating Expression.
    2. If ToBoolean(GetValue(exprRef)) is false, return (normal, V, empty).
red_while_2a_2b

While

  1. Repeat
    1. If ToBoolean(GetValue(exprRef)) is false, return (normal, V, empty).
red_while_2b_false

This Talk

JSCert Trust

Testing

Total #Test262 Tests
11746
Chapters 8-14
2782
#Passes in 8-14
1796
Total #Passes
2633
Remaining test failures due to: use of for-in, chapter 15 library use, the parser, buggy tests.

ES5 ↔ JSCert

Connecting ES5 to JSCert

JSCert ↔ JSRef

Connecting JSCert to JSRef

Bugs Found

This Talk

JSCert Trust
JSCert Trust
JSCert Trust

JSCert Statistics

ECMA Standard
280 pages
Declarative JSCert
3000 lines
Computable JSRef
2000 lines
Correctness Proof
3500 lines
Effort
8 people, part time, 1 year
URL
http://jscert.org

Try JSCert!