A Trusted Mechanised JavaScript Specification
Gareth Smith, Imperial College.
A Trusted Mechanised JavaScript Specification
http://jscert.org/popl14/
A Trusted Mechanised JavaScript Specification
Martin Bodin
Arthur Charguéraud
Alan Schmitt
Daniele Filaretti
Philippa Gardner
Sergio Maffeis
Daiva Naudziuniene
Gareth Smith
JavaScript Specifications
Initial Implementation (Netscape Navigator 1995)
ECMAScript 3 standard (1999)
Formal definition for the full language, justification via closeness to specification and proofs of safety properties (APLAS'08)
ECMAScript 5 (2009)
λ
JS
: translation into a λ-calculus with references, justification via testing (ECOOP'10)
Program logic for a core part of the language (POPL'12)
λS5: like λ
JS
for ES5 strict mode
F
*
to JavaScript via λ
JS
, a full abstraction result (POPL'13)
This Talk
Coverage
Coverage
ES5 ↔ JSCert
ES5 ↔ JSCert
ES5 ↔ JSCert
Reading the Coq
This:
Can be read as this:
While
Let
V
=
empty
.
Repeat
Let
exprRef
be the result of evaluating
Expression
.
If
ToBoolean
(
GetValue
(
exprRef
)) is
false
, return (
normal
,
V
,
empty
).
Let
stmt
be the result of evaluating
Statement
.
If
stmt
.value is not
empty
, let
V
=
stmt
.value.
If
stmt
.type is not
continue
||
stmt
.target is not in the current label set, then
If
stmt
.type is
break
and
stmt
.target is in the current label set, then
Return (
normal
,
V
,
empty
).
If
stmt
is an
abrupt completion
, return
stmt
.
While
Let
V
=
empty
.
While
Repeat
Let
exprRef
be the result of evaluating
Expression
.
If
ToBoolean
(
GetValue
(
exprRef
)) is
false
, return (
normal
,
V
,
empty
).
While
Repeat
If
ToBoolean
(
GetValue
(
exprRef
)) is
false
, return (
normal
,
V
,
empty
).
This Talk
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
JSCert ↔ JSRef
You can find the bisect report
here
.
Bugs Found
Finally completion values (SpiderMonkey, V8, WebKit).
for-in enumerates over properties deleted from prototype during enumeration (SpiderMonkey).
Dead code changing completion values (V8).
Shadowing non-enumerable properties still enumerated (V8, WebKit first reported by Mark Miller).
Typo in for-in spec (ES6).
Broken "informative algorithm" (ES6).
Underspecified Enumerate internal method (ES6).
Shadowing non-enumerable properties should not be enumerated (Test262).
No-one knows what test 12.6.4-2 is for (Test262).
NPE checking lg.proto (Test262).
This Talk
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!