[JSR308] Can we agree on our goals? (annotations on blocks)

[Gary T. Leavens]

Hi Eugene, and all,

Just a minor correction to your post.  JML doesn't need to restrict
users to only putting annotations on loop statements.  Indeed it could
be useful to annotate any statement.  The only reason I mentioned
loops explicitly is becuase that is more important to us than other
statements.  I would, however, prefer to be able to annotate all
kinds of Java statements.

While I'm at it, Tom's suggestion of annotating only blocks would be
acceptable for our purposes in JML.  My only objection to it is that
it's a bit irregular to only have annotations on declaration statements
and block statements.  But it would work for our use cases and has a
certain appeal (i.e., it's simple, and as Tom noted, it clearly
delimits the scope of the annotation).

On Thu, 1 Feb 2007, Eugene Kuleshov wrote:

> Tom Ball wrote:
>>>  Tom, does block nodes [in javac AST] have information about type of the 
>>> parent, i.e. if/else/for/try/catch/etc ?
>> No node has any knowledge of its parents, as javac's AST is a directed 
>> acyclic graph.  I'm not sure parent information is useful anyway since 
>> loop statements don't necessarily have blocks -- they have child 
>> statements which may or may not be blocks.
>> 
>> However, I was suggesting putting a block around the statement(s) to be 
>> annotated:
>> 
>>    @DoForever {
>>        for (;;) {
>>           ...
>>        }
>>    }
>> 
>> No parent node knowledge is needed here, whereas it would be a serious 
>> compiler whack to support something like "for (;;) @DoForever { ... }". 
>> IMHO, I think the former is easier to read.
> Yes, but "for (;;) @DoForever { ... }" meant postfix annotation linked to 
> the "for" not to the block. This is sensitive for tools like JML, because 
> they need to be able to restrict annotation on the loop only, but in your 
> suggestion nothing would stop user from doing something like this:
>
>  @DoForever {
>      for (;;) {
>         ...
>      }
>      doSomethingElse();
>  }
>
> On the other hand the following code would be valid (restricting block to 
> not change instance state for this particular scope):
>
>  @Readonly {
>      doSomething();
>      doSomethingElse();
>  }
>
> regards,
> Eugene
>
>
>
> _______________________________________________
> JSR308 mailing list
> JSR308 at lists.csail.mit.edu
> https://lists.csail.mit.edu/mailman/listinfo/jsr308
>


         Gary T. Leavens
         Department of Computer Science, Iowa State University
         229 Atanasoff Hall, Ames, Iowa 50011-1041 USA
         http://www.cs.iastate.edu/~leavens  phone: +1-515-294-1580