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 +1-514-848-2424 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
