Re: .jml file processing and refines clauses (was JML2: Inheritance of non-null parameter annotations)

[Werner Dietl]

Dear Patrice and David, all,

thanks for your replies.

> If you do not want to make any changes to the .java file then you need
> to rename the .jml to .refines-java.

I tried that and it still does not complain about inconsistencies with non-null
specifications.

The problem I'm having is the following: I want to add specifications,
e.g to the file
    java/util/Collection.spec
and then need to make sure that all subtypes are consistent, e.g
   java/util/List.spec
   java/util/ArrayList.refines-spec
At the moment, inconsistencies between these files seem to be ignored, for
example, if the signature for method "contains" uses different
nullity annotations, no error is reported.

Regards,
cu, WMD.



      ____________________________________________________________________________________
Be a better friend, newshound, and
know-it-all with Yahoo! Mobile.  Try it now.  http://mobile.yahoo.com/;_ylt=Ahu06i62sR8HDtDypao8Wcj9tAcJ

-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Gary T. Leavens-2]

Hi Werner, Patrice, David,

On Fri, 9 May 2008, Werner Dietl wrote:

> thanks for your replies.

Yes, thanks.

>> If you do not want to make any changes to the .java file then you need
>> to rename the .jml to .refines-java.
>
> I tried that and it still does not complain about inconsistencies with non-null
> specifications.

Did you also put in a refines directive at the top of the .refines-java file?

> The problem I'm having is the following: I want to add specifications,
> e.g to the file
>    java/util/Collection.spec
> and then need to make sure that all subtypes are consistent, e.g
>   java/util/List.spec
>   java/util/ArrayList.refines-spec
> At the moment, inconsistencies between these files seem to be ignored, for
> example, if the signature for method "contains" uses different
> nullity annotations, no error is reported.

In theory you should be able to put in Collections.refines-spec
something that says

  refines "Collection.spec";
  // ...

or you could just edit Collection.spec, of course.

         Gary T. Leavens
         210 Harris Center (Bldg. 116)
         School of EECS, University of Central Florida
         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
         http://www.eecs.ucf.edu/~leavens  phone: [phone]
         leavens@...

-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

Gary and Patrice were on the better track than I was in my original
comment, but I think some expansion on the way in which specification
files are processed would help.

The JML tools consider both the specification and the java implementation.

The java implementation of a class is found in the .java file, by
looking in the directories of the class path, in order.

The specification files are found as follows.  The directories of the
classpath (or source path or specspath) are searched in order for a file
with the right name and a suffix of .refines-java, .refines-spec,
.refines-jml, .java, .spec, or .jml.  This is considered the
Most-Refined-Compilation-Unit.  If there is more than one file with the
right name and an appropriate suffix in a directory, the file with the
suffix earlier in the list above is the MRCU.  Once a file is found, no
further directories are searched.

 From the MRCU, the chain of "refine" declarations is followed until one
gets to a file with no refine declaration.  This has the following
implications.
- only the specs in the MRCU and the files in the subsequent refinement
chain are considered.  There are various rules about how they are combined.
- if a .java and a .jml (or .spec) file are in the same directory, the
.java file is the MRCU; if the .java file does not have a refine
declaration, only the specs in the .java file are considered
- in general if the MRCU does not have a refine declaration, only the
specs in the MRCU are considered.  Any specs in the .java file (if it is
not the MRCU) are ignored (sometimes silently, depending on the tool).
- if the various .java and specification files are in different
directories, control of which of them is the MRCU can be exercied by
changing the classpath either intentionally or inadvertently.

I believe that the idea of a chain of refining files originated in the
desire to allow developers to increasingly refine a specification by
adding new files at the head of the refinement chain.  However, I do not
believe this is often used, if at all.  Specs are nearly always in a
single file - sometimes the .java file sometimes (as when specifying a
library) in a separate specification file.  Consequently the above seems
overly complicated.  However, if multiple specification files are to be
allowed but we do not have something like the refine declaration that
determines a refinement chain, it seems we would have to do a lot more
directory searching for appropriate files and devise other rules for
combining the multiple specification files. That seems worse than the
status quo.

A drastic simplification from the status quo would be to allow only one
specification file per class, perhaps change the suffix order, and warn
the user if there are specs in both a .java file and a specification file.

Another note: statements (e.g. loop invariants) that are embedded in the
body of a method are always found in the .java file.

Pet peeve: Since I like the .spec and .jml suffixes, I have always
wished that those suffixes preceded the .java suffix.

- David


-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Gary T. Leavens-2]

Hi David and all,

On Fri, 9 May 2008, David Cok wrote:

> Gary and Patrice were on the better track than I was in my original comment,
> but I think some expansion on the way in which specification files are
> processed would help.
>
> The JML tools consider both the specification and the java implementation.
>
> The java implementation of a class is found in the .java file, by looking in
> the directories of the class path, in order.
>
> The specification files are found as follows.  The directories of the
> classpath (or source path or specspath) are searched in order for a file with
> the right name and a suffix of .refines-java, .refines-spec, .refines-jml,
> .java, .spec, or .jml.  This is considered the Most-Refined-Compilation-Unit.
> If there is more than one file with the right name and an appropriate suffix
> in a directory, the file with the suffix earlier in the list above is the
> MRCU.  Once a file is found, no further directories are searched.
>
> From the MRCU, the chain of "refine" declarations is followed until one gets
> to a file with no refine declaration.  This has the following implications.
> - only the specs in the MRCU and the files in the subsequent refinement chain
> are considered.  There are various rules about how they are combined.
> - if a .java and a .jml (or .spec) file are in the same directory, the .java
> file is the MRCU; if the .java file does not have a refine declaration, only
> the specs in the .java file are considered
> - in general if the MRCU does not have a refine declaration, only the specs
> in the MRCU are considered.  Any specs in the .java file (if it is not the
> MRCU) are ignored (sometimes silently, depending on the tool).
> - if the various .java and specification files are in different directories,
> control of which of them is the MRCU can be exercied by changing the
> classpath either intentionally or inadvertently.

Yes, that's all correct, I believe.

> I believe that the idea of a chain of refining files originated in the desire
> to allow developers to increasingly refine a specification by adding new
> files at the head of the refinement chain.  However, I do not believe this is
> often used, if at all.  Specs are nearly always in a single file - sometimes
> the .java file sometimes (as when specifying a library) in a separate
> specification file.

We have used this feature for publication purposes, as in the
"Preliminary Design of JML" document, for breaking up a specification
into several parts.  But I agree this is not common and most often the
specification is just in one file.

> Consequently the above seems overly complicated.
> However, if multiple specification files are to be allowed but we do not have
> something like the refine declaration that determines a refinement chain, it
> seems we would have to do a lot more directory searching for appropriate
> files and devise other rules for combining the multiple specification files.
> That seems worse than the status quo.
>
> A drastic simplification from the status quo would be to allow only one
> specification file per class, perhaps change the suffix order, and warn the
> user if there are specs in both a .java file and a specification file.

This kind of simplification is something we should seriously consider
now, as we are redoing the basic tools.  I agree that the benefits of
such a simplification in terms of tools and teaching are significant
and thus I personally support such a simplication.  Would anyone's
specifications break horribly if we adopted this simplification?

> Another note: statements (e.g. loop invariants) that are embedded in the body
> of a method are always found in the .java file.

That's right.

> Pet peeve: Since I like the .spec and .jml suffixes, I have always wished
> that those suffixes preceded the .java suffix.

That is, that the MRCU would be in the .spec or .jml file.

         Gary T. Leavens
         210 Harris Center (Bldg. 116)
         School of EECS, University of Central Florida
         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
         http://www.eecs.ucf.edu/~leavens  phone: [phone]
         leavens@...

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Wladimir de Lara Araujo Filho]

        Hi, all,

        I agree with the simplifications.

        I have a question regarding the semantics of the application of
modifiers and refinement. For a type X declared in X.java and X.refines-spec
in which the latter includes the appropriate refine declaration, the nullity
modifiers on a method specification must match. However, this is not the
case for purity. X.refines-spec can declare a method pure that is not
declared so in the .java file. The reverse is not allowed.

        First, is there a reason for this inconsistency? Second, if there
isn't one, would there be a problem to have nullity behave the same as
purity w.r.t. refinement?

                Cheers,

Wladimir de Lara Araujo Filho
260 Besserer St. suite 602
Ottawa-ON Canada
K1N 1J3
Phone [phone]

There are three schools of magic.
One: State a tautology, then ring the changes on its
corollaries;  that's philosophy.
Two: Record many facts. Try to find a pattern.
Then make a wrong guess at the next fact; that's science.
Three: Be aware that you live in a malevolent Universe controlled
by Murphy's Law, sometimes offset by
Brewster's Factor; that's engineering.
-- Robert A. Heinlein

> -----Original Message-----
> From: jmlspecs-developers-bounces@... [mailto:jmlspecs-
> developers-bounces@...] On Behalf Of Gary T. Leavens
> Sent: May 12, 2008 1:48 PM
> To: David Cok
> Cc: JML developers list; JML interest list
> Subject: Re: [Jmlspecs-developers] .jml file processing and refines
> clauses
>
>
> This kind of simplification is something we should seriously consider
> now, as we are redoing the basic tools.  I agree that the benefits of
> such a simplification in terms of tools and teaching are significant
> and thus I personally support such a simplication.  Would anyone's
> specifications break horribly if we adopted this simplification?
>
> > Another note: statements (e.g. loop invariants) that are embedded in the
> body
> > of a method are always found in the .java file.
>
> That's right.
>
> > Pet peeve: Since I like the .spec and .jml suffixes, I have always
> wished
> > that those suffixes preceded the .java suffix.
>
> That is, that the MRCU would be in the .spec or .jml file.
>
>          Gary T. Leavens
>          210 Harris Center (Bldg. 116)
>          School of EECS, University of Central Florida
>          4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
>          http://www.eecs.ucf.edu/~leavens  phone: [phone]
>          leavens@...
>
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> _______________________________________________
> Jmlspecs-developers mailing list
> Jmlspecs-developers@...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Patrice Chalin-3]

Hello Wladimir, et al.,

Sorry for the delay in responding, it has been busy ...
> I have a question regarding the semantics of the application of
> modifiers and refinement. For a type X declared in X.java and X.refines-spec
> in which the latter includes the appropriate refine declaration, the nullity
> modifiers on a method specification must match. However, this is not the
> case for purity. X.refines-spec can declare a method pure that is not
> declared so in the .java file. The reverse is not allowed.
>
> First, is there a reason for this inconsistency?
The difference between nullity annotations and purity is that the
absence of a nullity annotation can be interpreted differently depending
on the class level modifiers and/or the compiler switch used.  Hence, as
far as I recall, when the "feature interaction" between nullity
annotations and specification refinement was considered, we decided that
nullities should match so as to avoid confusion. (Note that this doesn't
mean that explicit nullity modifiers are needed in all files of a
refinement chain. See e.g.
org/jmlspecs/checker/testcase/typecheck/NullableRefinement1.*)  I hope
this helps.

Cheers,
Patrice

--
Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof.
Dependable Software Research Group, CSE Department, Concordia University
Room EV3.215, Phone [phone] x3004. www.encs.concordia.ca/~chalin


-------------------------------------------------------------------------
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-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers