[JSR308] Annotations on statements (and expressions?)
Tom Ball
Tom.Ball at Sun.COM
Wed Jan 31 12:53:13 EST 2007
Let's get back to driving the spec via use-cases, and try to find a
balance between simplicity and completeness. There is a big jump
between small enhancements to improve detection of common program errors
versus support for complete specification of program behavior. For the
latter, I would recommend using a language like JML instead of Java, as
it looks very useful and well-designed. Having a common platform like
the JVM should allow developers more freedom to choose the appropriate
language(s) for their projects, rather than locking them into a single
language superset.
In general, I think too many people focus on changing Java instead of
coming up with better alternatives. The beauty of the JVM is that all
kinds of different languages can compile to it, or now with Java 6 can
be run via a scripting engine. I am happy to support standardizing the
draft's definition of new JVM class file attributes to enhance its
support for alternative languages, but am very reluctant to support
extending the Java language to the same degree.
As you might suspect, this discussion is pushing a button in me from a
horrible project disaster. I first joined Sun as a member of its new
CORBA platform. Management saw a need for a better application
environment, so it acquired the rights to NeXTStep to run on top of our
stack. NeXTStep is written in Objective C, so we worked with the gcc
folks to create a compiler that supported both languages. But rather
than switch between pure C++ and pure Objective C source files, the
compiler combined both languages into a superset of the two so a
developer could mix and match the parts of each language at will. While
both C++ and Objective C are fine development languages, this
superset-language caused complete chaos. As soon as I could, I
transferred to Sun's FirstPerson team; its attraction was its pragmatic,
simple language and platform called Oak, which was later renamed to
Java. I'd therefore like to keep the language true to its initial goal
of being a pragmatic application developer's first choice.
Tom
Gary T. Leavens wrote:
> Hi Tom and all,
>
> JML of course doesn't absolutely *need* support from Java for JML, and
> has done fine without direct support. One can of course add custom
> attributes to class files to record information, which works.
>
> The reason that JML would *like* support from Java for *syntax* is to
> make it easier to create tools to process (small) subsets of JML's
> notation, by writing contract syntax in Java annotations. Of course
> we can get by without this, and do currently. However, it seems that
> having a syntax based on annotations for JML or similar languages
> would have positive benefits for tool builders. On the other hand, if
> we can't use annotations uniformly for all assertions and contracts,
> in particular for loop invariants, then I would say that the pain of
> annotations (having to put everything in string literals) is not worth
> it for JML, as then JML would be even more non-uniform in its syntax
> than it already is. In that case I would argue that JML should make
> no or very little use of annotations.
>
> I thought this JSR was about syntax for adding annotations to more
> places in Java. Specification language contracts on statements (and
> loops in particular) are one instance of that. So that is why I've
> presented another use case for loop/statement annotations. You may of
> course not think that's compelling, but I certainly do, and I wanted
> to add it to the mix of other reasons for adding annotations on
> statements.
>
> On Wed, 31 Jan 2007, 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, as JVM
>> class files (should) already address that need. The JVM and Java core
>> classes make a great platform for researching new languages, and with
>> the open-source release of javac it is now even easier to create
>> them. If the JVM spec needs to be improved to support better
>> specification then either this JSR should focus on that issue, or a
>> new JSR should be created.
>>
>> Tom
>>
>> Gary T. Leavens wrote:
>>> Hi all,
>>>
>>> I wanted to point out another use for annotations on statements. For
>>> our work on specifications with the Java Modeling Language (JML, see
>>> http://jmlspecs.org), we would like to attach loop invariants to loop
>>> statements. This is actually my major reason for joining this JSR, as
>>> it's the biggest failing of Java's annotations for our work. For
>>> example, we'd like to write:
>>>
>>> int i = 0;
>>> int sum = 0;
>>>
>>> @maintaining("sum == (@sum int j; 0 <= j && j < i; a[j])")
>>> while (i < a.length) {
>>> sum += a[i];
>>> i++;
>>> }
>>>
>>> where the @maintaining annotation is attached to the while loop, and
>>> the @sum is not an annotation, but just something in the string in the
>>> annotation.
>>>
>>> Another use for this is to attach entire contracts to describe the
>>> effect
>>> of a statement (including loop statements), as this is often an aid to
>>> provers. For example, something like:
>>>
>>> @following(@spec_case(requires="i < Integer.MAX_VALUE",
>>> ensures="i == @old(i + 1)"))
>>> inc(i);
>>>
>>> (to take a very trivial example). That's less important to us, but
>>> would still be quite useful.
>>>
>>> For JML we don't usually need annotations on expressions, but we could
>>> definitely use annotations on new object construction expressions,
>>> such as
>>>
>>> new @Rep Document()
>>>
>>> I hope that something that could handle such examples would be
>>> acceptable to the group and the JCP. :-)
>>>
>>> On Tue, 30 Jan 2007, Neal Gafter wrote:
>>>
>>>> Annotations on statements? Annotations on expressions? It sounds
>>>> like the
>>>> scope of our work is exceeding the scope of the original proposal.
>>>>
>>>> I can imagine us wanting to support annotations on every sematically
>>>> meaningful nonterminal in the language, but I'm not sure a result along
>>>> those lines is likely to be acceptable by the JCP.
>>>>
>>>> On 1/30/07, Michael Ernst <mernst at csail.mit.edu> wrote:
>>>>>
>>>>> Trevor-
>>>>>
>>>>> Annotations on loops and other statements are within the scope of
>>>>> JSR 308,
>>>>> as noted by the current version of the proposal. However, no one
>>>>> has yet
>>>>> put forward a specific technical proposal for the syntax of
>>>>> loop/statement
>>>>> annotations (in Java and in the class file). Once someone does so,
>>>>> then
>>>>> we
>>>>> can evaluate that proposal and accept, improve, or reject it.
>>>>>
>>>>> I know that several other people, including Wayne Carr and Eugene
>>>>> Kuleshov
>>>>> (who responded separately to your message), are also interested in
>>>>> this
>>>>> topic. Perhaps you could join forces in preparing a proposal or at
>>>>> least
>>>>> preparing a statement that broaches the issues to the mailing list.
>>>
>>> I'd be happy to help with such a proposal...
>>>
>>> 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
>>>
>>>
>>> _______________________________________________
>>> JSR308 mailing list
>>> JSR308 at lists.csail.mit.edu
>>> https://lists.csail.mit.edu/mailman/listinfo/jsr308
>>
>>
>> _______________________________________________
>> 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
>
More information about the JSR308
mailing list