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

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