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: +1-407-823-4758
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
