Dear Gary,
On Sun, 2008-06-08 at 20:45 -0400, Gary T. Leavens wrote:
> Hi James,
>
> On Fri, 6 Jun 2008, Dr. James J. Hunt wrote:
>
> > Please forgive the delay in answering.
>
> No problem and likewise.
>
> > On Wed, 2008-06-04 at 13:12 -0400, Gary T. Leavens wrote:
> >> Hi James,
> >>
> >> On Wed, 4 Jun 2008, Dr. James J. Hunt wrote:
> >>
> >>> P.S. In general, I am interested in a JSR on converting JML to Metadata
> >>> Annotations, since our data flow analysis tool works with byte code.
> >>
> >> See the following TR for our design of this:
> >>
> >> Kristina Taylor's MS thesis at Iowa State this year discussed a design
> >> for this. You can get it from:
> >>
> >> ftp://ftp.cs.iastate.edu/pub/techreports/TR08-03
> >>
> >> Comments on that are welcome.
> >
> > I do not think the paper makes a convincing case for the level of
> > encoding in annotations that she chose. What makes annotations
> > interesting is that they are carried into the byte code. To make this
> > useful, they must drastically limit the parsing necessary. In
> > particular, one needs to know what are the Java variables referenced in
> > the clauses from the current method. I opine that to take anything but
> > the most radical approach she outlined will make it too difficult to
> > relate JML code fragments back to the byte code.
>
> Yes, I agree that having them in the byte code is important. I wish
> Java allowed interesting sturctures in annotations, but perhaps some
> more parsed form can be stored in the byte code.
Recursive annotation definitions would help a lot.
> But which do you mean by "the most radical approach"? Presumably not
> the middle one that she picked; I'm guessing you prefer the one that
> has the most fields fleshed out, what she calls the "clausal
> annotation". Is that right?
Yes
> Do you have a preferred way to relate the annotations to the variables
> in the Java code at the byte ode level?
This is a bit tricky, since the variable names do not necessarily exist
in the byte code and the registers in the byte code can not be
referenced at the source level. One way to do this would be to write
all expressions as methods. For example,
//@ descreasing a.size() - i;
whould become
@Decreasing("int foo(Collection a, int i) { return a.size() - i; }")
another would be to have a parameter list such as
@Decreasing(values="(Collection a, int i)", expression="a.size() - i")
or using annotation array syntax
@Decreasing(values={"Collection a", "int i"}, expression="a.size() - i")
One could even separate the types:
@Decreasing(types={"Collection", "int"},
names={"a", "i"},
value="a.size() - i")
but this gets rather verbose.
Perhaps a general expression would be best:
@Expression(type=decreasing,
values={"Collection a", "int i"},
body="a.size() - i")
where decreasing is a member of an ExpressionType enumeration.
In any case, the types are necessary to make it easy to generate a
synthetic class, calls to which could then be inject back into the byte
code.
> > For example, to analyze the initial value of a decreasing clause, we
> > inline the clause into the application code.
> >
> > Thus
> >
> > // @decreasing a.length() - i
> > for (int i = 0; i < a.length(); i++)
> > {
> > ...
> > }
>
> A minor but important confusion. In JML the // and the @ must be
> together, as in
>
> //@ decreasing a.length() - i;
> for (int i = 0; i < a.length(); i++)
> {
> // ...
> }
>
> Kristina's proposal uses Java 5 annotations, which unfortunately don't
> apply to statements. If they did, she would write this as (I believe):
>
> @Decreasing("a.length() - i")
> for (int i = 0; i < a.length(); i++)
> {
> // ...
> }
I opine that we should target JSR 308. Perhaps we can persuade the
group to add statement annotations. The alternative is to annotate the
loop variable, but that could get quite messy.
for (@Expression(type=decreasing,
values={"Collection a", "int i"},
body="a.size() - i")
int i = 0; i < a.size(); i++)
{
//...
}
> But perhaps better is to use your trick, transforming the JML in the
> bytecode to a call of some standard method:
>
> > can be transformed into
> >
> > {
> > int i = 0; // obtainable from the JML parser.
> > Do.nothing(a.length() - i);
> > }
> > for (int i = 0; i < a.length(); i++)
> > {
> > ...
> > }
> >
> > The value set for the Do.Nothing method gives the bound set for the
> > loop. Note that if a.length() grows in the loop, that the bound is
> > incorrect, but this can be shown with a deductive verifier tool such as
> > KeY.
>
> Good.
>
> > This trick does not work at the byte code level. It would very
> > difficult to parse the example and generate the equivalent byte code
> > without support form the annotations. Not to mention that the more
> > radical approach would benefit from better type and syntax checking from
> > javac.
>
> Again, I'm a bit clear on what you mean. I understand that you don't
> want to parse the bytecodes to recover this kind of structure. The
> alternative would be to have a table somewhere in the bytecode's
> auxiliary annotations that points out what byte codes are related to
> loop bounds. Thus a bytecode analyzer would just have to recover this information.
> Again, it's not clear how the radical aproach could help in Java 5 (or
> 6), since we can't attach annotaions to statements at all.
>
> Another possibililty, however, is to use some stereotyped declaration
> as a placeholder to add annotations to loops. For example, we've
> thought of something like transforming:
>
> //@ decreasing a.length() - i;
> for (int i = 0; i < a.length(); i++)
> {
> // ...
> }
>
> into:
>
> {
> int i=0;
> while (true) {
> long vf$0 = a.length() - i; // from the deccreasing clause
> if (i < a.length()) { break; }
> // ...
> i++;
> //@ assert 0 <= vf$0;
> //@ assert (a.length() - i) < vf$0;
> }
> }
>
> where vf$0 is the special name that could be searched for. We also
> had an encoding that is a bit more complex that keeps the loop as a
> for loop. (See earlier emails on the jmlspecs-interest list, which
> should be available on sourceforge.net in the archives; but there have
> been some problems with mailing list archives, so if you can't find
> that, let me know.)
Let us not be too tricky.
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
-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest
hunt-bounds.pdf (177K) 