nullness defaults for binaries

[davidcok]

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)?

• The default could be non_null because that is the general default in JML.
• The default could be nullable because to presume otherwise is unsound and would cause missed errors in verification. A user's incorrect assumption that the return value is non-null would not be corrected by a failing verification because the default was also wrong.

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.

[mattulbrich]

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.

[leavens]

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.

[davidcok]

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

• formal parameters take the fullness default in place for the class (typically non_null, but can be set with nullable_by_default)
• frame condition is assignable \everything
• reads condition is reads \everything
• return value, if a reference type, is nullable

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.

[leavens]

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.

[davidcok]

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)

[leavens]

Great, and it's fine with me to have reads be a synonym for accessible.

[mattulbrich]

• If you have no contract about a library method, you are in the soup anyway, so we can as well make that sound and as conservative as possible.
• ok for the synonym while I really got used to accessible in JML.

[leavens]

:-)