[Checkers] Spaces in commented JSR 308 annotations

Adam Kiezun akiezun at csail.mit.edu
Tue Jun 10 01:59:11 EDT 2008


It still feels like to me a strange and a bit gratuitous option.
It's a bit like having an option for allowing or disallowing multiple
spaces between keywords.
As a user of the framework, I don't think I want to think about this.
I think programmers should be able to be oblivious to whitespaces
(things should not stop working because I have a whitespace somewhere.
There are a few exceptions but it's hard to get them right: make got
it wrong, Python got it right).
Doesn't the compiler know which @ things are annotations and which are
not (from the classpath)?
If there are name conflicts with JML annotations, this options does
not solve them.

Just my 2 cents.
./adam

On Mon, Jun 9, 2008 at 9:48 PM, Michael Ernst <mernst at csail.mit.edu> wrote:
> Adam-
>
>> Why not have the compiler always  recognize the annotations? That is,
>> why would I not always want to use the option?
>
> It's funny you should ask.  I wrote an explanation in the manual, but then
> commented it out because I wanted to keep the manual short.
>
> This feature prevents the compiler from interpreting too many comments as
> annotations, since some comments that start with @ may not be annotations.
> For example, I've had trouble with pre-existing comments of the form "@
> symbolname" in JML-annotated code.
>
>                    -Mike
>



More information about the checkers mailing list