Lambda the Ultimate

inactiveTopic The Java™ specs in a formal way
started 12/9/2003; 3:34:27 AM - last post 12/18/2003; 10:16:49 AM
Andris Birkmanis - The Java™ specs in a formal way  blueArrow
12/9/2003; 3:34:27 AM (reads: 197, responses: 2)
After enjoying an old but still very actual Declarative Continuations and Categorical Duality paper, I felt an urge to reread The Java™ Language Specification (JLS), especially the part 14 (Blocks and Statements). This is where most of imperative nature lurks, and seems to be the part skipped by both Featherweight Java and Middleweight Java.

Citations from JLS:

The last section (§14.20) of this chapter addresses the requirement that every statement be reachable in a certain technical sense.

...

To be precise, a break statement with label Identifier always completes abruptly, the reason being a break with label Identifier. If no labeled statement with Identifier as its label encloses the break statement, a compile-time error occurs.

...

The preceding descriptions say “attempts to transfer control” rather than just “transfers control” because if there are any try statements (§14.19) within the break target whose try blocks contain the break statement, then any finally clauses of those try statements are executed, in order, innermost to outermost, before control is transferred to the break target. Abrupt completion of a finally clause can disrupt the transfer of control initiated by a break statement.

It all shows (to me, at least) how inefficient are natural language for specifications. JLS repeats clumsy baroque imprecise clauses in a natural language for 532 pages, where about 10 pages of precise denotational semantics would suffice. Do they really think it's easier for implementers to decypher their lawyerisms?

The definition of "reachability" takes about 5 pages. To me, it's just a matter of type system, which should not allow to compose non-returning "statement" with any would-be unreachable code.

I think that break, continue, and return could be nicely described in Filinski's terms. They are all just examples of dealing with non-local continuations lexically (as opposed to more prominent dynamic continuations aka unchecked exceptions). try, catch, finally, and throw would fit nicely into the same framework, without arcane “attempts to transfer control”.

Does anybody else share these concerns about current "best industry practices" in specifying languages?

PS: It amused me to find a hidden "DRAFT" watermark across the pages of JLS (was their finalization process limited to just making this invisible? :-) ).

Andris Birkmanis - Re: The Java™ specs in a formal way  blueArrow
12/11/2003; 4:25:21 AM (reads: 128, responses: 0)
A brand new bug I stumbled upon just today (courtesy Draw2d :-) ):

after executing the line:

prefSize.union(getLayoutManager().getPreferredSize(this, wHint, hHint));

the value of prefSize is null.

Why do I post it here? Because the person who wrote this code obviously assumed that if he/she called a method on a prefSize, it cannot be null immediately afterwards. It's so natural to assume that... But not correct :-(

To be honest, JLS warned you:

First, a target reference may be computed. Second, the argument expressions are evaluated.

And yes, for some (well meaning, no doubts) reasons, the getPreferredSize method modified the prefSize value.

So nothing new under the SUN, and everything is up to spec. Just not sure why "a target reference may be computed" but "the argument expressions are evaluated".

Frank Atanassow - Re: The Java™ specs in a formal way  blueArrow
12/18/2003; 10:16:49 AM (reads: 92, responses: 0)
Do they really think it's easier for implementers to decypher their lawyerisms?

I think part of the problem is: an informal definition takes ten times as long to read as a formal definition, but the reader can start learning about the subject matter right away; in contrast, to understand a formal definition you need to spend a sizable chunk of time up front to assimilate the notation and formalism, none of which has anything to do with the subject matter itself. So, though I think that a formal definition is more precise and unambiguous and usually takes less time to understand in total, it has a higher start-up cost, so to speak.

Oh, and of course 99% of programmers are afraid of formalisms which have never been published in any book with a drawing of an animal on its front cover.

Does anybody else share these concerns about current "best industry practices" in specifying languages?

Almost everybody in the programming language theory community. That's why we developed tools like operational semantics, type judgements, denotational semantics and so on.

Maybe someone needs to write an "Operational Semantics in a Nutshell" book?