« Return to Thread: Re: .jml file processing and refines clauses (was JML2: Inheritance of non-null parameter annotations)
Re: .jml file processing and refines clauses
by Gary T. Leavens-2
::
Rate this Message:
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: +1-407-823-4758
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
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: +1-407-823-4758
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
« Return to Thread: Re: .jml file processing and refines clauses (was JML2: Inheritance of non-null parameter annotations)
| Free Forum Powered by Nabble | Forum Help |
