Spec#, nullables and more

[bearophile]

Walter:

> Granted, even 100% coverage is no guarantee of no seg faults, but in practice it 
> is very effective.

Unittests are widely used in Java, still null exceptions are not uncommon in Java.


> And finally, null exceptions are not a bug. They are the messenger that there is 
> a bug in the code. Until one knows why a null pointer was dereferenced, one 
> cannot conclude that the existence of the null pointer was the bug.

I see, null exceptions are not a bug. But for the semantics of a part of a program it may be a bug to put a null inside a collection or inside a variable, or it may be a bug to pass a null to a certain function. Those are true bugs. A notnull type allows you to spot the bug, because the type system screams (if you have asked those things to be nonnull)

Your may write your function like this:
void foo(T@ x) {...}

it means T can't be null. As you say a segfault inside foo() is not a bug, the real bug is where that x was initialized, collected or created. The advantage of a nonnull type is that you will receive an error when you try to put a null inside the variable that will later be passed to foo(), this means where the true bug is. That foo() is also better than this:

void foo(T x)
  in { assert(x !is null); }
  body {...}

Because:
- You need to put a whole precondition there, while in the other case you just need to add a @. Less typing, etc.
- The test is done (or not done) at run-time. This slows down the function a little. In release mode you don't have the slowdown, but you lose the safety.
- The D contract system is not enforced at compile-time. This means that the true spot where the bug is, where the variable that later will become x is created, is not spotted. So your program will keep working until you call foo() and then a runtime exception or segfault will be generated. Instead if you are using a static type system, it means you are using that @ suffix, the type system statically spots the possible problem for you (it somehow forces you to put a nonnull inside the variable that will become x. At worst this will require a runtime test. But this test is done only once, if you later you call another function bar() with he same nonnull argument, it too will not need another runtime test).

Bye,
bearophile