about the official documents on such matters, the ECMAScript standard?
ECMAScript 3rd edition, the standard at the time, was around 180 pages long,
written in prose and pseudocode. Reading it didn't help much. It includes
gems such as this description of the
1. Let A be the list of CaseClause items in the first CaseClauses, in source text order. 2. For the next CaseClause in A, evaluate CaseClause. If there is no such CaseClause, go to step 7. 3. If input is not equal to Result(2), as defined by the !== operator, go to step 2. 4. Evaluate the StatementList of this CaseClause. 5. If Result(4) is an abrupt completion then return Result(4). 6. Go to step 13. 7. Let B be the list of CaseClause items in the second CaseClauses, in source text order. 8. For the next CaseClause in B, evaluate CaseClause. If there is no such CaseClause, go to step 15. 9. If input is not equal to Result(8), as defined by the !== operator, go to step 8. 10. Evaluate the StatementList of this CaseClause. 11. If Result(10) is an abrupt completion then return Result(10). 12. Go to step 18. ...
And this is just one of 180 pages of lesser or greater eloquence. With this as his formal reference, it's no wonder Arjun had a hard time making soundness claims.
As it turns out, Arjun and Claudiu did a pretty good job. λJS agrees with Mozilla SpiderMonkey on a few thousand lines of tests. We say "agreed" and not "passed" because SpiderMonkey fails some of its own tests. Without any other standard of correctness, λJS strives for bug-compatibility with SpiderMonkey on those tests.
Building on λJS
λJS is discussed in our ECOOP paper, but it's the work built on λJS that's most interesting. We've built the following systems ourselves:
- An extension to the above type-checker to verify ADsafe, as discussed in our USENIX Security 2011 paper.
- Others have a secret reimplementation of λJS in Java. We are now enterprise-ready.
match ECMAScript 5th ed. Our new semantics uses the official ECMAScript test
suite and tackles problems, such as
eval, that the original
λJS elided. We'll talk about it next time. Update:
We've written about our update, dubbed S5, its semantics for accessors,
and a particularly interesting