[Jsr308-statements] Comments on JSR 308 statements proposal

[Michael Ernst]

The JSR 308 statements proposal
(http://doc.ece.uci.edu/mediawiki/index.php/JSR-308_Statements) is a very
good start.  Thanks to everyone who worked on it!  Here are some comments:
I want to avoid stepping on others' toes by making large changes, and
others may be able to make them more efficiently than I.


The document conflates verification tools and defect detection tools.
These are not the same -- they have very different purposes.  FindBugs is
not a verification tool.  Being clear about the distinction does not weaken
the argument, but an inaccurate description will reduce credibility.

It's not clear what "to fully support annotations in these tools" means.
More annotation locations will make annotations more expressive; this lets
programmers express more, and can make the tools more effective.  But that
doesn't mean that those tools are useless now, which is what the statement
seems to suggest.

The structure of the "verification tools" section is confused, because it
does not indicate *what* is being verified.  That is more important than
where the annotations happen to appear.  For instance, the "statement
effects" section says "this is often an aid to provers", which at least
gives a hint as to what these are for.  The intro to the "concurrency,
atomicity, and parallelization" section is even better; this is what you
should be aiming for.

"For JML, it is necessary to attach loop invariants to loop statements" is
again unclear.  What is the task that this is necessary for?  Do you
really mean to say JML is useless without this capability?  Really, JML
assumes it for a particular purpose (give that), and currently JML uses
stylized comments.

Why are the code examples while loops?  While loops are usually worse style
than for loops, and the latter are easier to read.  It reduces the impact
of the document if the code examples use poor style.

The "collection classes" section has nothing to do with collection classes.
Its example adds nothing new, so cut it, or use it to replace the example
in the "loop invariants" section.  The key to this section is a the
discussion of "declarations are statements in Java, so programmers might
wonder why they cannot put annotations on all of the statements."  That
discussion is a good one.  However, it isn't a use case, but a different
variety of argument, so it belongs elsewhere.

"The framework can be automated" should be reworded for clarity, because a
framework isn't the sort of thing one automates.

"This field [pc field in bytecode] indicates the address in the bytecode at
which the statement begins."  Because the classfile needs to indicate
exactly which bytecodes are annotated, this is not enough.  Furthermore,
you need to discuss how you will handle compiler optimizations that may
reorder, duplicate, split, or move (parts of) statements.  This is one of
the key technical challenges, in my view.

Overall, I find that a document that makes its points in less space is
easier to read.  Readers are more likely to get all the way through, and
are more likely to understand the main points.  For example, you could
remove the attributions.  It's good to be scholarly and to give credit
where it is due, but I don't think they add much, except for the editors of
this document.  If you really want to retain them, add comments, or
footnotes at the end of the document.  Similarly, the "pros and cons"
statement at the end of the document can be shortened.  In my view, it's
better to express the arguments rather than give a historical description
of how the debate proceeded and who said what.

                    -Mike