Overspecification in JSCert - messages in native errors

[tilk]

Currently JSCert specifies that errors thrown with spec_error must have no message (rule red_spec_error).

But ES5 says that native errors have implementation-defined messages (15.11.7).

[charguer]

Hi,

We chose to drop implementation-defined parts.
But, ideally, all the development should be presented as a functor,
taking as argument a module that provides definitions and evaluation rules
for all implementation-specific parts.
I'm not sure how much of a priority that is, though.

Arthur

Currently JSCert specifies that errors thrown with spec_error must
have no message (rule red_spec_error).

But ES5 says that native errors have implementation-defined messages
(15.11.7).

—
Reply to this email directly or view it on GitHub
#14.

[tilk]

This makes JSCert less useful for other projects, such as the one I am doing. I'm now trying to prove S5 (the current version of lambdajs) correct with respect to JSCert, and this issue means either I leave some parts unproven, or I need to change S5 to follow the implementation decisions of JSRef.

I'm now confused about the philosophy of JSCert. I thought JSCert was supposed to be the formalized specification (and therefore only specify what is actually specified in the spec), and JSRef should be the runnable implementation (and therefore specify things left unspecified in JSCert). Was I wrong?

I'm confused about the functor idea. JSCert is presented as a predicate, and can therefore be non-deterministic in places where an implementation-dependent behavior can occur. Is this a bad idea for some reason?

[charguer]

Non-deterministic and implementation-dependent are two different things.

For example, you can have an implementation-dependent feature that has a
deterministic behavior.

This is why JSCert should be parametric in the implementation-dependent
features, rather than leaving transitions that may allow arbitrary
evaluation steps to be taken.

Does this help somehow?

This makes JSCert less useful for other projects, such as the one I am
doing. I'm now trying to prove S5 (the current version of lambdajs)
correct with respect to JSCert, and this issue means either I leave
some parts unproven, or I need to change S5 to follow the
implementation decisions of JSRef.

I'm now confused about the philosophy of JSCert. I thought JSCert was
supposed to be the formalized specification (and therefore only
specify what is actually specified in the spec), and JSRef should be
the runnable implementation (and therefore specify things left
unspecified in JSCert). Was I wrong?

I'm confused about the functor idea. JSCert is presented as a
predicate, and can therefore be non-deterministic in places where an
implementation-dependent behavior can occur. Is this a bad idea for
some reason?

—
Reply to this email directly or view it on GitHub
#14 (comment).

[tilk]

Thank you for the helpful response.

In this case, I think I will for now ignore the problem and document the places where I had to do that.

[Mbodin]

Hi,

I understand this idea of functors, but I have to admit that before
reading this thread, I really though that such functors should be
limited either to the interpretor, or to strange behaviours that does
not follow the specification (even if we take into account the places
where it’s allowed by the standard to to everything), like the proto
stuff.
I think that we should discuss about the meaning of
“implementation-defined”. Typically, if we states that a string is
“implementation-defined”, putting in the rules of JSCert some
non-determinism is perfectly OK for me (because my interpretation of
“implementation-defined” includes non determinism).
I’ve written one rule with this in mind, named
“red_spec_construct_string_2” that I think we should discuss... because
I probably had a different interpretation of all this than you have :-)

In a non-completely related matter, does someone know the difference
between “spec_error_spec” and “spec_error” (apart for the fact that the
first one is stuck if “spec_error” does not return a result... which if
intended should be explained somewhere :p)?

Martin.

[brabalan]

How about allowing any string or undefined?

  | red_spec_error : forall S C ne m s o1 o,
      (m = undef \/ m = prim_string s) ->
      red_expr S C (spec_build_error (prealloc_native_error_proto ne) m) o1 ->
      red_expr S C (spec_error_1 o1) o ->
      red_expr S C (spec_error ne) o

[tilk]

This would solve my issue, however it does introduce nondeterminism to the predicate.

[brabalan]

On 2015-05-22 16:48, Marek Materzok notifications@github.com writes:

This would solve my issue, however it does introduce nondeterminism to the
predicate.

Yes, which is one way to deal with implementation dependent matter. An
alternative would be to parameterize this.

Alan

OpenPGP Key ID : 040D0A3B4ED2E5C7

[IgnoredAmbience]

A closer reading of the standard for NativeErrors is leaving me unsettled:

15.11.6: Native Error Types Used in This Standard
One of the NativeError objects below is thrown when a runtime error is detected. All of these objects share the same structure, as described in 15.11.7.

15.11.7 NativeError Object Structure
When an ECMAScript implementation detects a runtime error, it throws an instance of one of the NativeError objects defined in 15.11.6.

My reading of this is that it throws the exact object as defined below (i.e. the constructor), this directly contradicts 15.11.7, which states that an instance should be thrown.

And to get back onto topic, the rest of 15.11.7 reads (emphasis mine)

Each of these objects has the structure described below, differing only in the name used as the constructor name instead of NativeError, in the name property of the prototype object, and in the implementation-defined message property of the prototype object.

NativeErrors are not defined to have a name own property, and the definition given is consistent with 15.11.7.9: NativeError.prototype.name:

The initial value of the name property of the prototype for a given NativeError constructor is the name of the constructor (the name used instead of NativeError).

Following this pattern, 15.11.7 says that NativeError.prototype.message is implementation-dependent.
However, this directly contradicts with 15.11.7.10 NativeError.prototype.message:

The initial value of the message property of the prototype for a given NativeError constructor is the empty string.

I believe the intent of the specification to be that the message own property of constructed instances to be implementation-dependent, but they've messed it up by adding the word "prototype" into the definition...

Thoughts?

[IgnoredAmbience]

The first of these issues has been corrected in ES6.
The wording of 15.11.7 (19.5.6 now) seems to remain the same.

[brabalan]

I would bring up such issues (the ones still present in ES6) on the es-discuss list. Are you subscribed?

[IgnoredAmbience]

I am subscribed, will take a brief look through test262 to see if I can find anything to support this before writing something along the lines of above.

[IgnoredAmbience]

It looks like the text in the spec is a hang-over from a change between ES3 and ES5, the text of 15.11.7.10 NativeError.prototype.message in ES3 is:

The initial value of the message property of the prototype for a given NativeError constructor is an implementation-defined string.

I'll report this directly to the ECMAScript bugtracker, since this appears to be the cause of the error.

[brabalan]

@edgemaster : I have a bugzilla account. Should I report it there (based on your email)? I’ll also ask Allen if he thinks it’s a bug.
edit: Allen confirmed it’s probably a bug, I’ll file it.