D allows inputs and outputs to have assertions placed on them.

i.e.

int f(int x){
  in{
    assert(even(x));
  }
  out{
    assert(odd(x));;
  }
}

I would like to know if D tries to statically check these assertions.  If so that would give a subtyping mechanism which would be kind of neat.

If not, consider the following scenario in addition to f.

int g(int x){
  in{
    assert(!odd(x));
  }
 ...
}

Suppose I made a call:

  g(f(x));

Can this be made to fail by composing the assertions?

Are there any tools or support for model checking and/or software verification in D outside of the core language (like Frama-C) that would support such analyses?

Jonathan:

> I would like to know if D tries to statically check these assertions.

Currently D doesn't statically verify them. I have an enhancement request in the works for something related, but it's not powerful enough for your use case.

Bye,
bearophile

>, but
> it's not powerful enough for your use case.
>
> Bye,
> bearophile

Is there a link available, so that I could see what is in the making?

Jonathan:

> Is there a link available, so that I could see what is in the making?

Yes, this is two thirds of my proposal:

http://www.digitalmars.com/d/archives/digitalmars/D/enum_pre-conditions_217595.html

Bye,
bearophile