[JSR308] Annotations on statements (and expressions?)

[Gary T. Leavens]

Hi Trevor and all,

Thanks, Trevor, for making those points, which are spot on.  JML in
its syntax is just a bunch of annotations added to Java.  Currently we
use /*@ ... @*/ and //@ "annotation comments" for such annotations.
It looks like these would also clash with the syntax used by such WCET
tools.

To repeat, if Java provides annotations on loop statements, then WCET
tools and specification langauges like JML can use them.  We don't
have to get any kind of agreement from Sun or Java or whoever on the
details of these annotations or their semantics.

On Wed, 31 Jan 2007, Trevor Harmon wrote:

> On Jan 31, 2007, at 8:34 AM, Tom Ball wrote:
>
>> I don't understand why a language like JML needs support from Java. 
>> There's no need to turn Java into an intermediate language
>
> Is JML truly a language? I thought it was really just annotations. So the 
> issue is not "How can language X be integrated into Java?" but rather "How 
> can annotation tool X use Java's annotation standard?" The latter question is 
> important because otherwise we have all these incompatible annotation 
> standards. For instance, tools that want to integrate with JML have to be 
> written specifically for JML's proprietary annotations. If JML could be built 
> to use Java's own annotation support, other tools could easily read and write 
> its annotations, and I suspect JML itself would be smaller and simpler. Also, 
> its annotation syntax would be consistent with the Java standard, which would 
> make it a bit nicer to use.
>
> WCET analysis tools face the same problem. Currently you find that every tool 
> has a completely different syntax to express exactly the same semantics. For 
> example, here's how you'd express loop bound annotations in some Java WCET 
> tools:
>
> Skånerost: /*$ loop-bound 100 */
> XAC: //@ Loopcount(100)
> WCA: //@ loop=100
>
> Because of the differing syntax, these statements are incompatible, even 
> though they all mean the same thing. If I were to write a lower-level WCET 
> tool, it would need to parse these annotations, and I'd have to write three 
> different parsers! Likewise, each new WCET tool has to bundle its own 
> annotation parser even if it were to use the same syntax as one of these 
> existing tools.
>
> Wouldn't it make much more sense if WCET tools standardized on Java's 
> built-in annotation support? But the problem for WCET tools is the same 
> problem Gary described for JML: There's no way to add an annotation on a 
> loop. Simply allowing this would go a long way toward convergence on a single 
> annotation standard.
>
> Trevor
>
>
> _______________________________________________
> 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