[Jsr308-statements] Question on the extent of a statement or block annotation

[Dr. James J. Hunt]

Dear Colleagues,

The wiki on statement annotations says the following in the section on
block annotations:

There is no representation of this source block in the bytecode, and
therefore the annotation data must include information about where it
begins and where it ends.

How is this different than statement annotations, except for the extent,
where the following is stated?

(TODO: Bytecode ranges are required even for simple statements: an
annotation on a statement (such as indicating locks, for example) must
be applied to every instruction generated from it, so incidating only
the initial instruction of a statement is inadequate. Because of
instruction reordering, a set of ranges is required. This section needs
to be restructured to present that from the beginning, and not to
suggest that blocks would require any differences in implementation
strategy.)

It seems that in both cases both a begin and an end are needed.

Furthermore, examples such as the following are not very persuasive,
since they are difficult to use at the byte code level because the parse
context is gone.  In particular, the variable names are not guarantee to
be preserved and the original parse context at that point in the code
needs to be recreated. 

int i;
int total = 0;
@maintaining("total == (@sum int j; 0 <= j && j < i; a[j])")
for (i = 0; i < a.length; i++) {
    total += a[i];
}

I am not saying that encoding JML statements in annotations is not a
useful goal in and off itself, but statement level annotations are
insufficient to give the power that one would like to have.  The ability
to have a general expression syntax is needed as well.  This requires
some form of recursive annotations.  I will make a more general comment
on this in the main mailing list.

We have a tool that uses the JML @decreases clause along with data flow
analysis at the byte code level to obtain concrete bounds for loops
without having to write application specific bounds into Java code.
There are a couple of workshop papers on the subject on our web site
under "http://www.aicas.com/sites/publications.html":
"http://www.aicas.com/papers/jtres_hunt_wceta.pdf" and
"http://www.aicas.com/papers/jtres_hunt_bounds.pdf".  The first paper
explains the difficulty of not having recursive annotations on
statements by showing a viable alternative that works but is quite
inelegant and the second gives a bases for why it is advantageous to
combine WCETA and JML.  If we were able to hand loop annootations
through to the byte code, it would make the interface much cleaner.

I do not much care if annotations are provided at the block level or the
statement level as either would be helpful to me.

Sincerely,
James

-- 
Dr. James J. Hunt      * CEO aicas group       * Tel: +49 721 663968 22

aicas incorporated
69 West Rock Ave.      * New Haven, CT 06515   * USA
http://www.aicas.com   * Tel: +1 203 676 9807  *

Business Filing Number: 0002879819, State of Connecticut
President: Dr. James J. Hunt, Secretary/Treasurer: David P. Reddy

aicas --- allerton interworks computer automated systems GmbH
Haid-und-Neu-Straße 18 * D-76131 Karlsruhe     * Deutschland (Germany)
http://www.aicas.com   * Tel: +49 721 663968 0 * FAX: +49 721 663968 99

USt-Id: DE216375633, Handelsregister HRB 109481, AG Mannheim
Geschäftsführer: Dr. James J. Hunt