Tuesday, December 24, 2013

Poor Usage of Language in the Specs

A snippet from JLS 7
http://docs.oracle.com/javase/specs/jls/se7/jls7.pdf

Section : 4.12.4 final Variables reads
A variable can be declared final. A final variable may only be assigned to once.
Declaring a variable final can serve as useful documentation that its value will
not change and can help avoid programming errors.
It is a compile-time error if a final variable is assigned to unless it is definitely
unassigned (§16) immediately prior to the assignment.

The lines marked in italics do not explain properly what the writer intends to speak.

The corrected version:

It is a compile-time error if a final variable is assigned to, unless it is definitely
unassigned (§16), immediately prior to the assignment.


Another Snippet From JLS 7

Section 17.5.1 Semantics of final Fields

What does these lines mean :

Is this paragraph even readable:


Let o be an object, and c be a constructor for o in which a final field f is written. A freeze action on final field f of o takes place when c exits, either normally or abruptly.
Note that if one constructor invokes another constructor, and the invoked constructor sets a final field, the freeze for the finalfield takes place at the end of the invoked constructor.
For each execution, the behavior of reads is influenced by two additional partial orders, the dereference chain dereferences() and the memory chain mc(), which are considered to be part of the execution (and thus, fixed for any particular execution). These partial orders must satisfy the following constraints (which need not have a unique solution):
  • Dereference Chain: If an action a is a read or write of a field or element of an object o by a thread t that did not initialize o, then there must exist some read r by thread t that sees the address of o such that r dereferences(r, a).
  • Memory Chain: There are several constraints on the memory chain ordering:
    • If r is a read that sees a write w, then it must be the case that mc(w, r).
    • If r and a are actions such that dereferences(r, a), then it must be the case that mc(r, a).
    • If w is a write of the address of an object o by a thread t that did not initialize o, then there must exist some read r by thread tthat sees the address of o such that mc(r, w).
Given a write w, a freeze f, an action a (that is not a read of a final field), a read r1 of the final field frozen by f, and a read r2 such that hb(w, f)hb(f, a)mc(a, r1), and dereferences(r1, r2), then when determining which values can be seen by r2, we consider hb(w, r2). (This happens-before ordering does not transitively close with other happens-before orderings.)
Note that the dereferences order is reflexive, and r1 can be the same as r2.
For reads of final fields, the only writes that are deemed to come before the read of the final field are the ones derived through the final field semantics.

What a piece of dirty, unfathomable spec writing.