Open davidcok opened 2 years ago
I validate the problem and agree that a decent set of assumption should apply. The non-null-result cannot be regarded in isolation. I think an even greater assumption is the framing condition of external code. Any method from outside must be annotated assignable \everything
in a conservative sound setting. That is a show-stopper at any rate.
I am okay with the proposal that the return value of a library function that has no specification should default to nullable
. I also agree that external (or native methods) should default to assignable \everything
in absence of a specification.
The nice thing about this is that it's easy to change the interpretation in particular cases by writing a specification.
OK. This is the agreement I think:
For a method with so source and no explicit specification (e.g. a library method), the default is
assignable \everything
reads \everything
The non-conservative diverges false
is the default for a missing diverges clause in an explicit specification. Shall we use that for a default specification also or fall back to the sound diverges true
?
I think in practice (because of the assignable \everything
) any library method that is called will need at least a bare-bones specification written, so perhaps the answer to the question on diverges does not matter too much.
That seems reasonable to me, although I believe you mean "no source" instead of "so source" and I would prefer "accessible \everything
" to "reads \everything
".
I think we should also settle on a sound default for diverges, so I would say to use diverges true
as the default for external methods with no specification. It is true that we will likely need to specify all library methods that are called in code we wish to verify.
I agree on the diverges true
default for binary classes.
Can we agree to have reads
be a synonym for accessible
? (reads
tends to be what is used in other languages)
Great, and it's fine with me to have reads
be a synonym for accessible
.
:-)
JML adopted a nonnull-by-default semantics some time ago.
I think it clear that this applies to user-written Java source code. In that case any JML tool can check that the source obeys such a specification and can annotate it accordingly if there are declarations that are allowed to be null.
My question is about library (binary) classes. Consider a library method that returns a reference. This being Java, the reference may or may not be null. Of course, we can always write a .jml specification that makes it clear whether the method may return null or not. But what should the default specification be for a binary, source-code-less class (without an explicit JML specification)?
I think I'm voting for the second policy for the default specification for binary classes, even though the default would now be different for binary and source classes.
Or to complicate things -- I'd be in favor of: formal parameters are non_null by default but return values are nullable by default, again, in the absence of any explicit specification or source code.