Spec#, nullables and more

[bearophile]

Walter Bright:

> "The current version of the Spec# program verifier does not check for arithmetic
> overflow."
> 
> Oh well!

Spec# comes from C# that I think has arithmetic overflows at runtime. So I think Spec# has runtime overflows. What that note about Spec# says is that Spec# is not yet able to verify statically (as SPARK does) that a function/program doesn't overflow.

Well, there is a way to know, you can use that "useless" site:
http://www.rise4fun.com/SpecSharp

And try this snippet:

class Example {
  int x;

  void Inc(int y)
    requires y > 0;
    ensures old(x) < x;
  {
    checked { x += y; }
  }
}

It compiles, so this quite probably means that Spec# has arithmetic overflows (because Spec# is a very strict compiler, it's not sloppy. Is surely signals as error the things it doesn't understand).
This also shows you why an online way to test programs is useful.

Anyway, the topic of this whole tread is about non-nullable types in D, copying from the very good implementation of Spec# (with the little changes I have shown).

Walter, instead of poking and teasing me as a ten year old does, why we don't start talking about serious things? Like, for example if we want nonnull references/pointers in D3. If you aren't interested in this feature we can stop wasting my time. It's not a necessary feature, I will keep using D2 even without it. But it may be something nice to have.

Bye,
bearophile